mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Submonoid.Defs
AddMonoidHom.eq_of_eqOn_topM : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {f g : M →+ N},
  Set.EqOn ⇑f ⇑g ↑⊤ → f = g
-- Mathlib.Data.List.Palindrome
List.Palindrome.cons_concat : ∀ {α : Type u_1} (x : α) {l : List α}, l.Palindrome → (x :: (l ++ [x])).Palindrome
-- Init.Data.Order.Opposite
Max.oppositeMin_def : ∀ {α : Type u_1} {min : Max α}, min.oppositeMin = { min := max }
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
/-- `lpMeas` and `Lp F p (μ.trim hm)` are isometric, with a linear equivalence.  -/
MeasureTheory.lpMeasToLpTrimLie : {α : Type u_1} →
  (F : Type u_2) →
    (𝕜 : Type u_3) →
      (p : ENNReal) →
        [inst : RCLike 𝕜] →
          [inst_1 : NormedAddCommGroup F] →
            [inst_2 : NormedSpace 𝕜 F] →
              {m m0 : MeasurableSpace α} →
                (μ : MeasureTheory.Measure α) →
                  [inst_3 : Fact (1 ≤ p)] →
                    (hm : m ≤ m0) → ↥(MeasureTheory.lpMeas F 𝕜 m p μ) ≃ₗᵢ[𝕜] ↥(MeasureTheory.Lp F p (μ.trim hm))
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.mod_eq_zero : ∀ {R : Type u} [inst : EuclideanDomain R] {a b : R}, a % b = 0 ↔ b ∣ a
-- Mathlib.Algebra.Order.Monovary
Monovary.add_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : PartialOrder β] {f₁ f₂ : ι → α} {g : ι → β}, Monovary f₁ g → Monovary f₂ g → Monovary (f₁ + f₂) g
-- Mathlib.Data.Bundle
Bundle.TotalSpace.mk_inj : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} {b : B} {y y' : E b}, ⟨b, y⟩ = ⟨b, y'⟩ ↔ y = y'
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.addSubgroupClass : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  AddSubgroupClass (Submodule R M) M
-- Mathlib.Data.PNat.Equiv
Equiv.pnatEquivNat_apply : ⇑Equiv.pnatEquivNat = PNat.natPred
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonCallHierarchyItem.toJson : Lean.Lsp.CallHierarchyItem → Lean.Json
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.setTR.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → ℕ → Array α → Sort u_2) (head : α) (xs : List α) (acc : Array α)
  (h_1 : (x : ℕ) → (x_1 : Array α) → motive [] x x_1)
  (h_2 : (head : α) → (xs : List α) → (acc : Array α) → motive (head :: xs) 0 acc)
  (h_3 : (x : α) → (xs : List α) → (n : ℕ) → (acc : Array α) → motive (x :: xs) n.succ acc),
  (match head :: xs, 0, acc with
    | [], x, x_1 => h_1 x x_1
    | head :: xs, 0, acc => h_2 head xs acc
    | x :: xs, n.succ, acc => h_3 x xs n acc) =
    h_2 head xs acc
-- Mathlib.CategoryTheory.Sites.CoversTop.Basic
/-- The section of a sheaf of types which lifts a compatible family of elements indexed
by objects which cover the terminal object.  -/
CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.section_ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {F : CategoryTheory.Functor Cᵒᵖ (Type w)} →
        {I : Type u_1} →
          {Y : I → C} →
            {x : CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y} →
              x.IsCompatible → J.CoversTop Y → CategoryTheory.Presheaf.IsSheaf J F → ↑F.sections
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.range_snd : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S),
  Set.range ⇑(CategoryTheory.Limits.pullback.snd f g) = ⇑g ⁻¹' Set.range ⇑f
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.l_comm_iff_u_comm : ∀ {X : Type u_2} [inst : PartialOrder X] {Y : Type u_3} [inst_1 : Preorder Y] {Z : Type u_4} [inst_2 : Preorder Z]
  {W : Type u_5} [inst_3 : PartialOrder W] {lYX : X → Y} {uXY : Y → X},
  GaloisConnection lYX uXY →
    ∀ {lWZ : Z → W} {uZW : W → Z},
      GaloisConnection lWZ uZW →
        ∀ {lWY : Y → W} {uYW : W → Y},
          GaloisConnection lWY uYW →
            ∀ {lZX : X → Z} {uXZ : Z → X},
              GaloisConnection lZX uXZ → ((∀ (w : W), uXZ (uZW w) = uXY (uYW w)) ↔ ∀ (x : X), lWZ (lZX x) = lWY (lYX x))
-- Mathlib.RingTheory.Smooth.Basic
Algebra.formallySmooth_iff : ∀ (R : Type u) (A : Type v) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.FormallySmooth R A ↔ Module.Projective A Ω[A⁄R] ∧ Subsingleton (Algebra.H1Cotangent R A)
-- Mathlib.Probability.Decision.Risk.Basic
ProbabilityTheory.avgRisk_le_iSup_risk : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} (ℓ : Θ → 𝓨 → ENNReal) (P : ProbabilityTheory.Kernel Θ 𝓧) (κ : ProbabilityTheory.Kernel 𝓧 𝓨)
  (π : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure π],
  ProbabilityTheory.avgRisk ℓ P κ π ≤ ⨆ θ, ∫⁻ (y : 𝓨), ℓ θ y ∂(κ.comp P) θ
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toSpanSingleton_smul : ∀ (R₁ : Type u_1) [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] [inst_4 : TopologicalSpace R₁] [inst_5 : ContinuousSMul R₁ M₁] {α : Type u_9}
  [inst_6 : Monoid α] [inst_7 : DistribMulAction α M₁] [inst_8 : ContinuousConstSMul α M₁]
  [inst_9 : SMulCommClass R₁ α M₁] (c : α) (x : M₁),
  ContinuousLinearMap.toSpanSingleton R₁ (c • x) = c • ContinuousLinearMap.toSpanSingleton R₁ x
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoState.mk.inj : ∀ {enabled : Bool} {assignment : Lean.PersistentHashMap Lean.MVarId Lean.Elab.InfoTree}
  {lazyAssignment : Lean.PersistentHashMap Lean.MVarId (Task Lean.Elab.InfoTree)}
  {trees : Lean.PersistentArray Lean.Elab.InfoTree} {enabled_1 : Bool}
  {assignment_1 : Lean.PersistentHashMap Lean.MVarId Lean.Elab.InfoTree}
  {lazyAssignment_1 : Lean.PersistentHashMap Lean.MVarId (Task Lean.Elab.InfoTree)}
  {trees_1 : Lean.PersistentArray Lean.Elab.InfoTree},
  { enabled := enabled, assignment := assignment, lazyAssignment := lazyAssignment, trees := trees } =
      { enabled := enabled_1, assignment := assignment_1, lazyAssignment := lazyAssignment_1, trees := trees_1 } →
    enabled = enabled_1 ∧ assignment = assignment_1 ∧ lazyAssignment = lazyAssignment_1 ∧ trees = trees_1
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullHom'Hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  (D : F.DescentData' sq sq₃) {Y : C} (q : Y ⟶ S) (i₁ i₂ : ι) (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂)
  (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q) (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q),
  CategoryTheory.IsIso (CategoryTheory.Pseudofunctor.DescentData'.pullHom' D.hom q f₁ f₂ hf₁ hf₂)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map_equiv_top : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M ≃+ N), AddSubsemigroup.map ↑f ⊤ = ⊤
-- Std.Data.Iterators.Producers.Repeat
Std.Iterators.Types.RepeatIterator.mk.sizeOf_spec : ∀ {α : Type u} {f : α → α} [inst : SizeOf α] (next : α), sizeOf { next := next } = 1 + sizeOf next
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_maxKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {he : t ≠ ∅}, t.getKey! (t.maxKey he) = t.maxKey he
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum' : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (t : Set α), μ t = ∑' (g : G), μ (t ∩ (g +ᵥ s))
-- Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
MeasureTheory.empty_mem_closedCompactCylinders : ∀ {ι : Type u_1} (X : ι → Type u_2) [inst : (i : ι) → TopologicalSpace (X i)],
  ∅ ∈ MeasureTheory.closedCompactCylinders X
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- A partial map from a reduced scheme to a separated scheme is equivalent to a morphism
if and only if it is equal to the restriction of the morphism.  -/
AlgebraicGeometry.Scheme.PartialMap.equiv_toPartialMap_iff_of_isSeparated : ∀ {X Y S : AlgebraicGeometry.Scheme} [inst : X.Over S] [inst_1 : Y.Over S] [AlgebraicGeometry.IsReduced X]
  [AlgebraicGeometry.IsSeparated (Y ↘ S)] {f : X.PartialMap Y} {g : X ⟶ Y}
  [AlgebraicGeometry.Scheme.PartialMap.IsOver S f] [AlgebraicGeometry.Scheme.Hom.IsOver g S],
  f.equiv (AlgebraicGeometry.Scheme.Hom.toPartialMap g) ↔ f.hom = CategoryTheory.CategoryStruct.comp f.domain.ι g
-- Init.Data.Int.Gcd
Int.pow_dvd_pow_iff : ∀ {a b : ℤ} {n : ℕ}, n ≠ 0 → (a ^ n ∣ b ^ n ↔ a ∣ b)
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Complete
/-- Assuming the existence of certain limits, functors into a monoidal closed category form a
monoidal closed category.

Note: this is defined completely abstractly, and does not have any good definitional properties.
See the TODO in the module docstring.
 -/
CategoryTheory.Functor.functorCategoryMonoidalClosed : (I : Type u₂) →
  [inst : CategoryTheory.Category.{v₂, u₂} I] →
    (C : Type u₁) →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [CategoryTheory.MonoidalClosed C] →
            [∀ (F : CategoryTheory.Functor (CategoryTheory.Discrete I) C),
                  (CategoryTheory.Discrete.functor id).HasRightKanExtension F] →
              [CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingParallelPair C] →
                CategoryTheory.MonoidalClosed (CategoryTheory.Functor I C)
-- Batteries.Data.String.Lemmas
/-- Validity for a string iterator.  -/
String.Legacy.Iterator.Valid : String.Legacy.Iterator → Prop
-- Mathlib.LinearAlgebra.Matrix.IsDiag
Matrix.IsDiag.smul : ∀ {α : Type u_1} {R : Type u_3} {n : Type u_4} [inst : Zero α] [inst_1 : SMulZeroClass R α] (k : R) {A : Matrix n n α},
  A.IsDiag → (k • A).IsDiag
-- Init.Data.BitVec.Basic
/-- Shifts all bits of `x` to the left by `1` and sets the least significant bit to `b`.

This is a non-dependent version of `BitVec.concat` that does not change the total bitwidth.
 -/
BitVec.shiftConcat : {n : ℕ} → BitVec n → Bool → BitVec n
-- Init.Omega.Int
Lean.Omega.Int.le_lt_asymm : ∀ {x y : ℤ}, y ≤ x → x < y → False
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
/-- The inclusion `BifibrantObject C ⥤ FibrantObject C`, as a localizer morphism.  -/
HomotopicalAlgebra.BifibrantObject.ιFibrantObjectLocalizerMorphism : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      CategoryTheory.LocalizerMorphism (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.BifibrantObject C))
        (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.FibrantObject C))
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- A noncomputable Euclidean domain structure on a discrete valuation ring, where the GCD algorithm
only takes two steps to terminate. Given `GCD(x,y)`, if `x ∣ y` then `y%x = 0` so we're done in one
step; otherwise `y%x = y` and then `GCD(x,y) = GCD(y,x)` which brings us back to the first case.
See `EuclideanDomain.to_principal_ideal_domain` for EuclideanDomain ⇒ PID.  -/
IsDiscreteValuationRing.toEuclideanDomain : (R : Type u_2) → [inst : CommRing R] → [inst_1 : IsDomain R] → [IsDiscreteValuationRing R] → EuclideanDomain R
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.pow_mod_orderOf_cycleOf_apply : ∀ {α : Type u_2} (f : Equiv.Perm α) [inst : DecidableRel f.SameCycle] (n : ℕ) (x : α),
  (f ^ (n % orderOf (f.cycleOf x))) x = (f ^ n) x
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.Λ'.normal.injEq : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (a a_1 : Λ),
  (Turing.TM1to1.Λ'.normal a = Turing.TM1to1.Λ'.normal a_1) = (a = a_1)
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.mk.sizeOf_spec : ∀ {J : Type u} [inst : LinearOrder J] [inst_1 : SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  [inst_2 : SizeOf J] (succ : (j : J) → ¬IsMax j → F.obj (Opposite.op j) → F.obj (Opposite.op (Order.succ j)))
  (map_succ :
    ∀ (j : J) (hj : ¬IsMax j) (x : F.obj (Opposite.op j)),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) (succ j hj x) = x)
  (lift : (j : J) → Order.IsSuccLimit j → ↑(⋯.functor.op.comp F).sections → F.obj (Opposite.op j))
  (map_lift :
    ∀ (j : J) (hj : Order.IsSuccLimit j) (x : ↑(⋯.functor.op.comp F).sections) (i : J) (hi : i < j),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) (lift j hj x) =
        ↑x (Opposite.op ⟨i, hi⟩)),
  sizeOf { succ := succ, map_succ := map_succ, lift := lift, map_lift := map_lift } = 1
-- Mathlib.GroupTheory.Congruence.Opposite
AddCon.op.eq_1 : ∀ {M : Type u_1} [inst : Add M] (c : AddCon M),
  c.op = { r := fun a b => c (AddOpposite.unop b) (AddOpposite.unop a), iseqv := ⋯, add' := ⋯ }
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.InductionObj.instCoeFunInductionObjForallFinPolynomial : {R : Type u_2} →
  [inst : CommRing R] → {n : ℕ} → CoeFun (ChevalleyThm.PolynomialC.InductionObj✝ R n) fun x => Fin n → Polynomial R
-- Batteries.Tactic.Congr
Batteries.Tactic.Congr.Config.mk.inj : ∀ {closePre closePost closePre_1 closePost_1 : Bool},
  { closePre := closePre, closePost := closePost } = { closePre := closePre_1, closePost := closePost_1 } →
    closePre = closePre_1 ∧ closePost = closePost_1
-- Mathlib.NumberTheory.FunctionField
FunctionField.ringOfIntegers.instIsIntegralClosureSubtypeMemSubalgebraPolynomial : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra (Polynomial F) K],
  IsIntegralClosure (↥(FunctionField.ringOfIntegers F K)) (Polynomial F) K
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.ofFractionRing_smul : ∀ {K : Type u} [inst : CommRing K] {R : Type u_1} [inst_1 : SMul R (FractionRing (Polynomial K))] (c : R)
  (p : FractionRing (Polynomial K)), { toFractionRing := c • p } = c • { toFractionRing := p }
-- Lean.CoreM
Lean.Core.CoreM.toIO' : {α : Type} → Lean.CoreM α → Lean.Core.Context → Lean.Core.State → IO α
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIdsM.Context.mk.injEq : ∀ (commonMCtx? : Option Lean.MetavarContext) (mctx₁ mctx₂ : Lean.MetavarContext) (allowAssignmentDiff : Bool)
  (commonMCtx?_1 : Option Lean.MetavarContext) (mctx₁_1 mctx₂_1 : Lean.MetavarContext) (allowAssignmentDiff_1 : Bool),
  ({ commonMCtx? := commonMCtx?, mctx₁ := mctx₁, mctx₂ := mctx₂, allowAssignmentDiff := allowAssignmentDiff } =
      { commonMCtx? := commonMCtx?_1, mctx₁ := mctx₁_1, mctx₂ := mctx₂_1,
        allowAssignmentDiff := allowAssignmentDiff_1 }) =
    (commonMCtx? = commonMCtx?_1 ∧ mctx₁ = mctx₁_1 ∧ mctx₂ = mctx₂_1 ∧ allowAssignmentDiff = allowAssignmentDiff_1)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_self_eq_one_iff : ∀ {b : ℝ}, Real.logb b b = 1 ↔ b ≠ 0 ∧ b ≠ 1 ∧ b ≠ -1
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
/-- Given the subspaces `p q`, if `p.quotient ≃ₗ[K] q`, then `q.quotient ≃ₗ[K] p`  -/
FiniteDimensional.LinearEquiv.quotEquivOfQuotEquiv : {K : Type u} →
  {V : Type v} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] → [FiniteDimensional K V] → {p q : Subspace K V} → ((V ⧸ p) ≃ₗ[K] ↥q) → (V ⧸ q) ≃ₗ[K] ↥p
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsIsometricSMul.mk : ∀ {M : Type u} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : SMul M X],
  (∀ (c : M), Isometry fun x => c • x) → IsIsometricSMul M X
-- Mathlib.Algebra.Polynomial.Div
Polynomial.eval_divByMonic_pow_rootMultiplicity_ne_zero : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} (a : R),
  p ≠ 0 → Polynomial.eval a (p /ₘ (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p) ≠ 0
-- Lean.Meta.Tactic.Grind.EMatch
/-- Checks constraints of the form `lhs =/= rhs` and `lhs =?= rhs`.
`expectedResult` is `true` if `lhs` and `rhs` should be definitionally equal.
 -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.checkDefEq : Bool → List Lean.Name → List Lean.Level → Array Lean.Expr → ℕ → Lean.Meta.Grind.CnstrRHS → Lean.Meta.Grind.GoalM Bool
-- Lean.LibrarySuggestions.SymbolFrequency
/-- Helper function for running `MetaM` code during module export, when there is nothing but an `Environment` available.
Panics on errors.
 -/
_private.Lean.LibrarySuggestions.SymbolFrequency.0.Lean.Environment.unsafeRunMetaM : {α : Type} → [Inhabited α] → Lean.Environment → Lean.MetaM α → α
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instCommSemiring : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : AddCommMonoid Γ] →
      [inst_1 : PartialOrder Γ] → [IsOrderedCancelAddMonoid Γ] → [inst : CommSemiring R] → CommSemiring (HahnSeries Γ R)
-- Init.SizeOf
UInt16.ofBitVec.sizeOf_spec : ∀ (toBitVec : BitVec 16), sizeOf { toBitVec := toBitVec } = 1 + sizeOf toBitVec
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsCartesian.map_self : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsCartesian f φ],
  CategoryTheory.Functor.IsCartesian.map p f φ φ = CategoryTheory.CategoryStruct.id a
-- Mathlib.Order.WithBot
WithTop.top_ne_coe : ∀ {α : Type u_1} {a : α}, ⊤ ≠ ↑a
-- Mathlib.Analysis.Asymptotics.TVS
/-- **Alias** of the reverse direction of `Asymptotics.isThetaTVS_iff_isTheta`. -/
Asymptotics.IsTheta.isThetaTVS : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : SeminormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E]
  [inst_4 : NormedSpace 𝕜 F] {f : α → E} {g : α → F} {l : Filter α}, f =Θ[l] g → f =Θ[𝕜; l] g
-- Mathlib.Order.ModularLattice
IsLowerModularLattice.mk : ∀ {α : Type u_2} [inst : Lattice α], (∀ {a b : α}, a ⋖ a ⊔ b → a ⊓ b ⋖ b) → IsLowerModularLattice α
-- Mathlib.Data.Int.GCD
_private.Mathlib.Data.Int.GCD.0.Nat.P.match_1.eq_1 : ∀ (motive : ℕ × ℤ × ℤ → Sort u_1) (r : ℕ) (s t : ℤ) (h_1 : (r : ℕ) → (s t : ℤ) → motive (r, s, t)),
  (match (r, s, t) with
    | (r, s, t) => h_1 r s t) =
    h_1 r s t
-- Init.Data.SInt.Basic
instShiftRightISize : ShiftRight ISize
-- Init.Data.SInt.Lemmas
Int16.sub_mul : ∀ {a b c : Int16}, (a - b) * c = a * c - b * c
-- Mathlib.RingTheory.RootsOfUnity.Minpoly
/-- The reduction modulo `p` of the minimal polynomial of a root of unity `μ` is squarefree.  -/
IsPrimitiveRoot.squarefree_minpoly_mod : ∀ {n : ℕ} {K : Type u_1} [inst : CommRing K] {μ : K},
  IsPrimitiveRoot μ n →
    ∀ [IsDomain K] [CharZero K] {p : ℕ} [inst_3 : Fact (Nat.Prime p)],
      ¬p ∣ n → Squarefree (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ μ))
-- Mathlib.Analysis.Complex.Trigonometric
Complex.ofReal_tanh_ofReal_re : ∀ (x : ℝ), ↑(Complex.tanh ↑x).re = Complex.tanh ↑x
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.id_left_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C)
  (X_1 : SimplexCategoryᵒᵖ),
  (CategoryTheory.CategoryStruct.id X).left.app X_1 = CategoryTheory.CategoryStruct.id (X.left.obj X_1)
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.Boundary.fst_inj : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} {ac : e₁.AreComplementary e₂} {i₁ i₁' : ι₁} {i₂ : ι₂},
  ac.Boundary i₁ i₂ → ac.Boundary i₁' i₂ → i₁ = i₁'
-- Mathlib.CategoryTheory.Action.Monoidal
Action.diagonalSuccIsoTensorTrivial.eq_1 : ∀ (G : Type u) [inst : Group G],
  Action.diagonalSuccIsoTensorTrivial G 0 =
    Action.diagonalOneIsoLeftRegular G ≪≫
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor (Action.leftRegular G)).symm ≪≫
        CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.Iso.refl (Action.leftRegular G))
          (Action.tensorUnitIso (Equiv.ofUnique PUnit.{u + 1} (Fin 0 → G)).toIso)
-- Mathlib.CategoryTheory.Sites.LeftExact
CategoryTheory.GrothendieckTopology.preservesLimits_diagramFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{t, w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  (X : C) [CategoryTheory.Limits.HasLimitsOfSize.{max t u v, max t u v, t, w} D],
  CategoryTheory.Limits.PreservesLimits (J.diagramFunctor D X)
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.coe_unitGroupMulEquiv_symm_apply : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (a : (↥A)ˣ), ↑↑(A.unitGroupMulEquiv.symm a) = ↑↑a
-- Mathlib.Order.Filter.EventuallyConst
Filter.HasBasis.eventuallyConst_iff : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} {ι : Sort u_5} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → (Filter.EventuallyConst f l ↔ ∃ i, p i ∧ ∀ x ∈ s i, ∀ y ∈ s i, f x = f y)
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instToJsonTextDocumentSyncKind : Lean.ToJson Lean.Lsp.TextDocumentSyncKind
-- Lean.DocString.Types
Lean.Doc.Inline.link.inj : ∀ {i : Type u} {content : Array (Lean.Doc.Inline i)} {url : String} {content_1 : Array (Lean.Doc.Inline i)}
  {url_1 : String},
  Lean.Doc.Inline.link content url = Lean.Doc.Inline.link content_1 url_1 → content = content_1 ∧ url = url_1
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteResidueField.mk_eq_mk : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K]
  {x y : ArchimedeanClass.FiniteElement K},
  ArchimedeanClass.FiniteResidueField.mk x = ArchimedeanClass.FiniteResidueField.mk y ↔
    0 < ArchimedeanClass.mk (↑x - ↑y)
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.interSmallerFnₘ.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3) (kv' : (a : α) × β a)
  (h_1 : (kv' : (a : α) × β a) → motive (some kv')) (h_2 : Unit → motive none),
  (match some kv' with
    | some kv' => h_1 kv'
    | none => h_2 ()) =
    h_1 kv'
-- Lean.DocString.Parser
/-- Are newlines allowed here?  -/
Lean.Doc.Parser.InlineCtxt.allowNewlines : Lean.Doc.Parser.InlineCtxt → Bool
-- Mathlib.CategoryTheory.Abelian.Injective.Extend
CategoryTheory.InjectiveResolution.instIsLECochainComplexOfNatInt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  (R : CategoryTheory.InjectiveResolution X), R.cochainComplex.IsLE 0
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- The top affine subspace is linearly equivalent to the affine space.
This is the affine version of `Submodule.topEquiv`.  -/
AffineSubspace.topEquiv : (k : Type u_1) →
  (V : Type u_2) →
    (P : Type u_3) →
      [inst : Ring k] → [inst_1 : AddCommGroup V] → [inst_2 : Module k V] → [S : AddTorsor V P] → ↥⊤ ≃ᵃ[k] P
-- Mathlib.Data.Finset.NAry
Finset.image₂_left : ∀ {α : Type u_1} {β : Type u_3} {s : Finset α} {t : Finset β} [inst : DecidableEq α],
  t.Nonempty → Finset.image₂ (fun x x_1 => x) s t = s
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.instPowSubtypeMemAddSubgroupInt : {R : Type u_1} → [inst : Field R] → [inst_1 : StarRing R] → Pow ↥(selfAdjoint R) ℤ
-- Init.Data.Array.Sort.Lemmas
Subarray.toList_mergeSort : ∀ {α : Type u_1} {xs : Subarray α} {le : α → α → Bool}, (xs.mergeSort le).toList = (Std.Slice.toList xs).mergeSort le