mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Vertex.VertexOperator
/-- A vertex operator over a commutative ring `R` is an `R`-linear map from an `R`-module `V` to
Laurent series with coefficients in `V`.  We write this as a specialization of the heterogeneous
case.  -/
VertexOperator : (R : Type u_3) → (V : Type u_4) → [inst : CommRing R] → [inst_1 : AddCommGroup V] → [Module R V] → Type u_4
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.isOrtho_zero_left : ∀ {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [inst : CommSemiring R]
  [inst_1 : CommSemiring R₁] [inst_2 : AddCommMonoid M₁] [inst_3 : Module R₁ M₁] [inst_4 : CommSemiring R₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₂ M₂] [inst_7 : AddCommMonoid M] [inst_8 : Module R M] {I₁ : R₁ →+* R}
  {I₂ : R₂ →+* R} (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M) (x : M₂), B.IsOrtho 0 x
-- Mathlib.Topology.Path
Path.truncate_self : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} (γ : Path a b) (t : ℝ),
  γ.truncate t t = (Path.refl (γ.extend t)).cast ⋯ ⋯
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.torsionOrder_eq_two_of_odd_finrank : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K],
  Odd (Module.finrank ℚ K) → NumberField.Units.torsionOrder K = 2
-- Mathlib.Topology.Order.LocalExtr
IsLocalMin.inf : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SemilatticeInf β] {f g : α → β} {a : α},
  IsLocalMin f a → IsLocalMin g a → IsLocalMin (fun x => f x ⊓ g x) a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.maxKey!_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α} {f : β → β},
  (Std.DTreeMap.Const.modify t k f).isEmpty = false →
    (Std.DTreeMap.Const.modify t k f).maxKey! = if cmp t.maxKey! k = Ordering.eq then k else t.maxKey!
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.mk.inj : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} {inst : Group G} {inst_1 : MulAction G X}
  {ps : DiscreteTiling.Protoset G X ιₚ} {index : ιₚ}
  {groupElts : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index)).subtype (↑ps index).symmetries} {index_1 : ιₚ}
  {groupElts_1 : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index_1)).subtype (↑ps index_1).symmetries},
  { index := index, groupElts := groupElts } = { index := index_1, groupElts := groupElts_1 } →
    index = index_1 ∧ groupElts ≍ groupElts_1
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExProdNat.brecOn.go : {motive_1 : (e : Q(ℕ)) → Mathlib.Tactic.Ring.Common.ExBaseNat e → Sort u} →
  {motive_2 : (e : Q(ℕ)) → Mathlib.Tactic.Ring.Common.ExProdNat e → Sort u} →
    {motive_3 : (e : Q(ℕ)) → Mathlib.Tactic.Ring.Common.ExSumNat e → Sort u} →
      {e : Q(ℕ)} →
        (t : Mathlib.Tactic.Ring.Common.ExProdNat e) →
          ((e : Q(ℕ)) → (t : Mathlib.Tactic.Ring.Common.ExBaseNat e) → t.below → motive_1 e t) →
            ((e : Q(ℕ)) → (t : Mathlib.Tactic.Ring.Common.ExProdNat e) → t.below → motive_2 e t) →
              ((e : Q(ℕ)) → (t : Mathlib.Tactic.Ring.Common.ExSumNat e) → t.below → motive_3 e t) →
                motive_2 e t ×' t.below
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
/-- If a set of ae strongly measurable functions is stable under addition and approximates
characteristic functions in `ℒp`, then it is dense in `ℒp`.  -/
MeasureTheory.MemLp.induction_dense : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α},
  p ≠ ⊤ →
    ∀ (P : (α → E) → Prop),
      (∀ (c : E) ⦃s : Set α⦄,
          MeasurableSet s →
            μ s < ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ g, MeasureTheory.eLpNorm (g - s.indicator fun x => c) p μ ≤ ε ∧ P g) →
        (∀ (f g : α → E), P f → P g → P (f + g)) →
          (∀ (f : α → E), P f → MeasureTheory.AEStronglyMeasurable f μ) →
            ∀ {f : α → E},
              MeasureTheory.MemLp f p μ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ g, MeasureTheory.eLpNorm (f - g) p μ ≤ ε ∧ P g
-- Mathlib.Topology.UniformSpace.Cauchy
/-- A set `s` is totally bounded if for every entourage `d` there is a finite
set of points `t` such that every element of `s` is `d`-near to some element of `t`.  -/
TotallyBounded : {α : Type u} → [uniformSpace : UniformSpace α] → Set α → Prop
-- Mathlib.FieldTheory.FinTrdeg
instFinTrdegOfEssFiniteType : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Algebra.EssFiniteType K L],
  FinTrdeg K L
-- Mathlib.Combinatorics.HalesJewett
/-- The main color of an almost monochromatic line.  -/
Combinatorics.Line.AlmostMono.color : {α : Type u_5} → {ι : Type u_6} → {κ : Type u_7} → {C : (ι → Option α) → κ} → Combinatorics.Line.AlmostMono C → κ
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.noZeroSMulDivisors_of_prime_of_degree_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [IsDomain R],
  Prime f → f.degree ≠ 0 → Module.IsTorsionFree R (AdjoinRoot f)
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The indexing set of cells of the subcomplex.  -/
Topology.RelCWComplex.Subcomplex.I : {X : Type u_1} →
  [t : TopologicalSpace X] →
    {C D : Set X} →
      [inst : Topology.RelCWComplex C D] →
        Topology.RelCWComplex.Subcomplex C → (n : ℕ) → Set (Topology.RelCWComplex.cell C n)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.normAtAllPlaces_mixedSpaceOfRealSpace : ∀ {K : Type u_1} [inst : Field K] {x : NumberField.mixedEmbedding.realSpace K},
  (∀ (w : NumberField.InfinitePlace K), 0 ≤ x w) →
    NumberField.mixedEmbedding.normAtAllPlaces (NumberField.mixedEmbedding.mixedSpaceOfRealSpace x) = x
-- Mathlib.CategoryTheory.Groupoid.Discrete
CategoryTheory.instIsGroupoidOfIsDiscrete : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.IsDiscrete C],
  CategoryTheory.IsGroupoid C
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalGroup.IsSES.integral_inducedMeasure : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Group A] [inst_1 : Group B] [inst_2 : Group C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →* B} {ψ : B →* C}
  (H : TopologicalGroup.IsSES φ ψ) [inst_6 : IsTopologicalGroup A] [inst_7 : IsTopologicalGroup B]
  [inst_8 : MeasurableSpace A] [inst_9 : BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsHaarMeasure]
  [inst_10 : IsTopologicalGroup C] [inst_11 : LocallyCompactSpace B] [inst_12 : MeasurableSpace C]
  [inst_13 : BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsHaarMeasure] [inst_14 : T2Space B]
  [inst_15 : MeasurableSpace B] [inst_16 : BorelSpace B] (f : CompactlySupportedContinuousMap B ℝ),
  ∫ (b : B), f b ∂H.inducedMeasure μA μC = (H.integrate μA μC) f
-- Mathlib.GroupTheory.OreLocalization.Basic
_private.Mathlib.GroupTheory.OreLocalization.Basic.0.AddOreLocalization.vadd'_char : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X] (r₁ : R) (r₂ : X) (s₁ s₂ u : ↥S) (v : R),
  ↑u + r₁ = v + ↑s₂ → AddOreLocalization.vadd'✝ r₁ s₁ r₂ s₂ = (v +ᵥ r₂) -ₒ (u + s₁)
-- Mathlib.SetTheory.Lists
Lists'.Subset.brecOn : ∀ {α : Type u_1} {motive_1 : (a a_1 : Lists α) → a.Equiv a_1 → Prop}
  {motive_2 : (a a_1 : Lists' α true) → a.Subset a_1 → Prop} {a a_1 : Lists' α true} (t : a.Subset a_1),
  (∀ (a a_2 : Lists α) (t : a.Equiv a_2), t.below → motive_1 a a_2 t) →
    (∀ (a a_2 : Lists' α true) (t : a.Subset a_2), t.below → motive_2 a a_2 t) → motive_2 a a_1 t
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.homogeneousComponent_mul_of_le_order : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f g : MvPowerSeries σ R} {p q : ℕ},
  ↑p ≤ f.order →
    ↑q ≤ g.order →
      (MvPowerSeries.homogeneousComponent (p + q)) (f * g) =
        (MvPowerSeries.homogeneousComponent p) f * (MvPowerSeries.homogeneousComponent q) g
-- Mathlib.Geometry.Manifold.Riemannian.Basic
enorm_tangentSpace_vectorSpace : ∀ {F : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x : F}
  {v : TangentSpace (modelWithCornersSelf ℝ F) x}, ‖v‖ₑ = ‖v‖ₑ
-- Mathlib.Topology.Algebra.Monoid
instContinuousMulMultiplicativeOfContinuousAdd : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Add M] [ContinuousAdd M], ContinuousMul (Multiplicative M)
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- A morphism of homological complexes consists of maps between the chain groups,
commuting with the differentials.
 -/
HomologicalComplex.Hom : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} → HomologicalComplex V c → HomologicalComplex V c → Type (max u_1 v)
-- Mathlib.MeasureTheory.Function.AEEqOfLIntegral
MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  {f g : α → ENNReal},
  Measurable f →
    Measurable g →
      (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ) → f =ᵐ[μ] g
-- Mathlib.Topology.Algebra.Algebra
/-- Under a dense continuous algebra map, a subalgebra
whose `TopologicalClosure` is `⊤` is sent to another such submodule.
That is, the image of a dense subalgebra under a map with dense range is dense.
 -/
DenseRange.topologicalClosure_map_subalgebra : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : IsSemitopologicalSemiring A] [inst_8 : IsSemitopologicalSemiring B] {f : A →A[R] B},
  DenseRange ⇑f → ∀ {s : Subalgebra R A}, s.topologicalClosure = ⊤ → (Subalgebra.map (↑f) s).topologicalClosure = ⊤
-- Mathlib.Order.CountableSupClosed
mem_countableSupClosure_iff : ∀ {α : Type u_2} {s : Set α} {a : α} [inst : Preorder α],
  a ∈ countableSupClosure s ↔ ∃ A, ∃ (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsLUB A a
-- Lean.Declaration
Lean.Constructor.mk.inj : ∀ {name : Lean.Name} {type : Lean.Expr} {name_1 : Lean.Name} {type_1 : Lean.Expr},
  { name := name, type := type } = { name := name_1, type := type_1 } → name = name_1 ∧ type = type_1
-- Mathlib.Algebra.Algebra.Opposite
AlgEquiv.toLinearEquiv_toOpposite : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A],
  ↑(AlgEquiv.toOpposite R A) = MulOpposite.opLinearEquiv R
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.isEqvAux.eq_2 : ∀ {α : Type u} (xs ys : Array α) (hsz : xs.size = ys.size) (p : α → α → Bool) (i : ℕ) (h : i + 1 ≤ xs.size),
  xs.isEqvAux ys hsz p i.succ h = (p xs[i] ys[i] && xs.isEqvAux ys hsz p i ⋯)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_congr : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m.WF → ∀ {a b : α}, (a == b) = true → Std.DHashMap.Raw.Const.get! m a = Std.DHashMap.Raw.Const.get! m b
-- Mathlib.Topology.FiberBundle.Basic
FiberPrebundle.continuous_trivChange : ∀ {B : Type u_2} {F : Type u_3} {E : B → Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : (x : B) → TopologicalSpace (E x)] (self : FiberPrebundle F E),
  ∀ e ∈ self.pretrivializationAtlas,
    ∀ e' ∈ self.pretrivializationAtlas, ContinuousOn (↑e ∘ ↑e'.symm) (e'.target ∩ ↑e'.symm ⁻¹' e.source)
-- Mathlib.Tactic.Linarith.Datatypes
/-- A preprocessor transforms a proof of a proposition into a proof of a different proposition.
The return type is `List Expr`, since some preprocessing steps may create multiple new hypotheses,
and some may remove a hypothesis from the list.
A "no-op" preprocessor should return its input as a singleton list.
 -/
Mathlib.Tactic.Linarith.Preprocessor : Type
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.nontrivial : ∀ {d : ℤ}, Nontrivial (ℤ√d)
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapHomologyIso'_inv_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.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S₁.HasHomology]
  [inst_6 : S₂.HasHomology] [inst_7 : (S₁.map F).HasHomology] [inst_8 : (S₂.map F).HasHomology]
  [inst_9 : F.PreservesRightHomologyOf S₁] [inst_10 : F.PreservesRightHomologyOf S₂] {Z : D}
  (h : (S₂.map F).homology ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.homologyMap φ))
      (CategoryTheory.CategoryStruct.comp (S₂.mapHomologyIso' F).inv h) =
    CategoryTheory.CategoryStruct.comp (S₁.mapHomologyIso' F).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (F.mapShortComplex.map φ)) h)
-- Mathlib.Analysis.Normed.Module.Basic
/-- Produces a `SeminormedAddCommGroup E` instance from a `SeminormedSpace.Core` on a type
that already has a preexisting uniform space structure and a preexisting bornology. This requires
proofs that the uniformity induced by the norm is equal to the preexisting uniformity, and likewise
for the bornology. See note [reducible non-instances].  -/
SeminormedAddCommGroup.ofCoreReplaceAll : {𝕜 : Type u_6} →
  {E : Type u_7} →
    [inst : NormedField 𝕜] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Norm E] →
          [inst_3 : Module 𝕜 E] →
            [U : UniformSpace E] →
              [B : Bornology E] →
                (core : SeminormedSpace.Core 𝕜 E) →
                  uniformity E = uniformity E →
                    (∀ (s : Set E), Bornology.IsBounded s ↔ Bornology.IsBounded s) → SeminormedAddCommGroup E
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.symm_h : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H), b.symm.h = -b.h
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoid.End.instOne : (M : Type u_4) → [inst : AddZero M] → One (AddMonoid.End M)
-- Std.Time.Date.PlainDate
Std.Time.instLawfulEqOrdPlainDate : Std.LawfulEqOrd Std.Time.PlainDate
-- Mathlib.Algebra.GroupWithZero.Action.TransferInstance
/-- Transfer `MulActionWithZero` across an `Equiv`  -/
Equiv.mulActionWithZero : (M₀ : Type u_2) →
  {A : Type u_3} →
    {B : Type u_4} →
      (e : A ≃ B) → [inst : MonoidWithZero M₀] → [inst_1 : Zero B] → [MulActionWithZero M₀ B] → MulActionWithZero M₀ A
-- Mathlib.Algebra.Order.Monovary
AntivaryOn.div_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : PartialOrder β] {s : Set ι} {f₁ f₂ : ι → α} {g : ι → β},
  AntivaryOn f₁ g s → MonovaryOn f₂ g s → AntivaryOn (f₁ / f₂) g s
-- Lean.Parser.Term
Lean.Parser.Term.quotedName.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Calculus.ContDiff.RCLike
/-- If `f` is `C^1` within a convex set `s` at `x`, then it is Lipschitz on a neighborhood of `x`
within `s`.  -/
ContDiffWithinAt.exists_lipschitzOnWith : ∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f : E → F} {s : Set E} {x : E},
  ContDiffWithinAt ℝ 1 f s x → Convex ℝ s → ∃ K, ∃ t ∈ nhdsWithin x s, LipschitzOnWith K f t
-- Mathlib.Geometry.Euclidean.Circumcenter
Affine.Simplex.circumcenter.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n), s.circumcenter = s.circumsphere.center
-- Init.Prelude
/-- Returns the number of bytes required to encode this `Char` in UTF-8.  -/
Char.utf8Size : Char → ℕ
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getEntryLE? : {α : Type u} → {β : α → Type v} → [Ord α] → α → Std.DTreeMap.Internal.Impl α β → Option ((a : α) × β a)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
/-- The multicospan index obtained by applying a functor.  -/
CategoryTheory.Limits.MulticospanIndex.map : {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] →
        {J : CategoryTheory.Limits.MulticospanShape} →
          CategoryTheory.Limits.MulticospanIndex J C →
            CategoryTheory.Functor C D → CategoryTheory.Limits.MulticospanIndex J D
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instReprCompletionItemKind.repr : Lean.Lsp.CompletionItemKind → ℕ → Std.Format
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- `vecMulVec` as a bilinear map.

When `A` is noncommutative, `R` and `S` can be instantiated as `vecMulVecBilin A Aᵐᵒᵖ`.  -/
vecMulVecBilin : {m : Type u_2} →
  {n : Type u_3} →
    (R : Type u_4) →
      (S : Type u_5) →
        {A : Type u_6} →
          [inst : Semiring R] →
            [inst_1 : Semiring S] →
              [inst_2 : NonUnitalNonAssocSemiring A] →
                [inst_3 : Module R A] →
                  [inst_4 : Module S A] →
                    [inst_5 : SMulCommClass S R A] →
                      [SMulCommClass S A A] → [IsScalarTower R A A] → (m → A) →ₗ[R] (n → A) →ₗ[S] Matrix m n A
-- Mathlib.RingTheory.Unramified.LocalStructure
Algebra.IsUnramifiedAt.congr_simp : ∀ (R : Type u_1) {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (q q_1 : Ideal A)
  (e_q : q = q_1) [inst_3 : q.IsPrime], Algebra.IsUnramifiedAt R q = Algebra.IsUnramifiedAt R q_1
-- Lean.Meta.Sym.Simp.SimpM
/-- Pre-computed `.rfl` results to avoid dynamic memory allocation.
Each combination of `done` and `contextDependent` maps to a compile-time constant.
 -/
Lean.Meta.Sym.Simp.mkRflResult : optParam Bool false → optParam Bool false → Lean.Meta.Sym.Simp.Result
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.map_top_of_surjective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N),
  Function.Surjective ⇑f → Subgroup.map f ⊤ = ⊤
-- Mathlib.CategoryTheory.Join.Pseudofunctor
/-- The pseudofunctor sending `D` to `C ⋆ D`.  -/
CategoryTheory.Join.pseudofunctorRight : (C : Type u₁) →
  [CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Pseudofunctor CategoryTheory.Cat CategoryTheory.Cat
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- The canonical injection of G's generators into G  -/
IsFreeGroup.of : {G : Type u_1} → [inst : Group G] → [inst_1 : IsFreeGroup G] → IsFreeGroup.Generators G → G
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.ofRat_inv : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : DivisionRing β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (x : β),
  CauSeq.Completion.ofRat x⁻¹ = (CauSeq.Completion.ofRat x)⁻¹
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.order_mul : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] [NoZeroDivisors R] {x y : HahnSeries Γ R},
  x ≠ 0 → y ≠ 0 → (x * y).order = x.order + y.order
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.ext_iff : ∀ {X Y : AddSemigrp} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.GroupTheory.Sylow
Sylow.conj_eq_normalizer_conj_of_mem : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G)
  [_hP : IsMulCommutative ↥↑P] (x g : G),
  x ∈ P → g⁻¹ * x * g ∈ P → ∃ n ∈ Subgroup.normalizer ↑P, g⁻¹ * x * g = n⁻¹ * x * n
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.instT0Space : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : TopologicalSpace X] [T0Space X],
  T0Space (Metric.Snowflaking X α hα₀ hα₁)
-- Init.Data.UInt.Lemmas
USize.toUInt8_ofNatLT : ∀ {n : ℕ} (hn : n < USize.size), (USize.ofNatLT n hn).toUInt8 = UInt8.ofNat n
-- Mathlib.SetTheory.Ordinal.Rank
IsWellFounded.rank_eq_typein : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r], IsWellFounded.rank r = ⇑(Ordinal.typein r).toRelEmbedding
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropyInf_eq_iSup_basis : ∀ {X : Type u_1} [inst : UniformSpace X] {ι : Sort u_2} {p : ι → Prop} {s : ι → SetRel X X},
  (uniformity X).HasBasis p s →
    ∀ (T : X → X) (F : Set X),
      Dynamics.coverEntropyInf T F = ⨆ i, ⨆ (_ : p i), Dynamics.coverEntropyInfEntourage T F (s i)
-- Lean.Language.Basic
_private.Lean.Language.Basic.0.Lean.Language.Snapshot.Diagnostics.mk.injEq : ∀ (msgLog : Lean.MessageLog) (interactiveDiagsRef? : Option (IO.Ref (Option Dynamic))) (msgLog_1 : Lean.MessageLog)
  (interactiveDiagsRef?_1 : Option (IO.Ref (Option Dynamic))),
  ({ msgLog := msgLog, interactiveDiagsRef? := interactiveDiagsRef? } =
      { msgLog := msgLog_1, interactiveDiagsRef? := interactiveDiagsRef?_1 }) =
    (msgLog = msgLog_1 ∧ interactiveDiagsRef? = interactiveDiagsRef?_1)
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.pointwiseAddCommMonoid : {R : Type u_2} →
  {M : Type u_3} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → AddCommMonoid (Submodule R M)
-- Mathlib.RingTheory.GradedAlgebra.TensorProduct
AlgHom.liftEquiv.congr_simp : ∀ (R : Type u_4) (S : Type u_5) (A : Type u_6) (B : Type u_7) [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R A] [inst_5 : Algebra S B] [inst_6 : Algebra R S]
  [inst_7 : Algebra R B] [inst_8 : IsScalarTower R S B], AlgHom.liftEquiv R S A B = AlgHom.liftEquiv R S A B
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.HasStrictTerminalObjects.out : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasStrictTerminalObjects C]
  {I A : C} (f : I ⟶ A) (a : CategoryTheory.Limits.IsTerminal I), CategoryTheory.IsIso f
-- Mathlib.Computability.PartrecCode
/-- Recursion on `Nat.Partrec.Code` is primitive recursive.  -/
Nat.Partrec.Code.primrec_recOn : ∀ {α : Type u_1} {σ : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable σ] {c : α → Nat.Partrec.Code},
  Primrec c →
    ∀ {z : α → σ},
      Primrec z →
        ∀ {s : α → σ},
          Primrec s →
            ∀ {l : α → σ},
              Primrec l →
                ∀ {r : α → σ},
                  Primrec r →
                    ∀ {pr : α → Nat.Partrec.Code → Nat.Partrec.Code → σ → σ → σ},
                      (Primrec fun a => pr a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2) →
                        ∀ {co : α → Nat.Partrec.Code → Nat.Partrec.Code → σ → σ → σ},
                          (Primrec fun a => co a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2) →
                            ∀ {pc : α → Nat.Partrec.Code → Nat.Partrec.Code → σ → σ → σ},
                              (Primrec fun a => pc a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2) →
                                ∀ {rf : α → Nat.Partrec.Code → σ → σ},
                                  (Primrec fun a => rf a.1 a.2.1 a.2.2) →
                                    have F := fun a c =>
                                      Nat.Partrec.Code.recOn c (z a) (s a) (l a) (r a) (pr a) (co a) (pc a) (rf a);
                                    Primrec fun a => F a (c a)
-- Aesop.Tree.Data
Aesop.NormalizationState.provenByNormalization.sizeOf_spec : ∀ (postState : Lean.Meta.SavedState) (script : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep))),
  sizeOf (Aesop.NormalizationState.provenByNormalization postState script) = 1 + sizeOf postState + sizeOf script
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_ringHom_ofRingHom : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S) (g : S →+* R)
  (h₁ : f.comp g = RingHom.id S) (h₂ : g.comp f = RingHom.id R), ↑(RingEquiv.ofRingHom f g h₁ h₂) = f