mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.id_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : AlgebraicGeometry.SheafedSpace C),
  (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id X.toPresheafedSpace
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.pullback₃.map_p₃_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)],
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₃ hf₁ f₂ f₃))
      f₃ =
    CategoryTheory.Functor.relativelyRepresentable.pullback₃.π hf₁ f₂ f₃
-- Lean.Compiler.LCNF.Types
Lean.Compiler.«term◾» : Lean.ParserDescr
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots.le_of_dvd : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p q : Polynomial R}, q ≠ 0 → p ∣ q → p.roots ≤ q.roots
-- Mathlib.CategoryTheory.Category.Pairwise
/-- Given a function `U : ι → α` for `[CompleteLattice α]`,
`iSup U` provides a cocone over `diagram U`.
 -/
CategoryTheory.Pairwise.cocone : {ι : Type v} →
  {α : Type u} →
    (U : ι → α) → [inst : CompleteLattice α] → CategoryTheory.Limits.Cocone (CategoryTheory.Pairwise.diagram U)
-- Init.Data.ByteArray.Lemmas
ByteArray.toByteArray_eq_empty : ∀ {l : List UInt8}, l.toByteArray = ByteArray.empty ↔ l = []
-- Mathlib.ModelTheory.Basic
/-- Not an instance to avoid a loop.  -/
FirstOrder.Language.HomClass.strongHomClassOfIsAlgebraic : ∀ {L : FirstOrder.Language} [L.IsAlgebraic] {F : Type u_3} {M : Type u_4} {N : Type u_5} [inst : L.Structure M]
  [inst_1 : L.Structure N] [inst_2 : FunLike F M N] [L.HomClass F M N], L.StrongHomClass F M N
-- Mathlib.Topology.Category.Profinite.Nobeling.Induction
Profinite.NobelingProof.GoodProducts.linearIndependent : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [WellFoundedLT I],
  IsClosed C → LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.eval C)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.selRightfAction_actionUnitIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x : C),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso x =
    CategoryTheory.MonoidalCategoryStruct.rightUnitor x
-- Mathlib.RingTheory.Ideal.Height
/-- `dim R ≤ n` if and only if the height of all maximal ideals is less than `n`.  -/
ringKrullDim_le_iff_isMaximal_height_le : ∀ {R : Type u_2} [inst : CommRing R] (n : WithBot ℕ∞), ringKrullDim R ≤ n ↔ ∀ ⦃m : Ideal R⦄, m.IsMaximal → ↑m.height ≤ n
-- Mathlib.Topology.Category.Compactum
/-- The functor `compactumToCompHaus` is an equivalence of categories.  -/
compactumToCompHaus.isEquivalence : compactumToCompHaus.IsEquivalence
-- Mathlib.Order.Interval.Set.Basic
Set.mem_Iic_of_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a x : α}, x ∈ Set.Iio a → x ∈ Set.Iic a
-- Mathlib.FieldTheory.Perfect
/-- A perfect field of characteristic `p` (prime) is a perfect ring.  -/
PerfectField.toPerfectRing : ∀ {K : Type u_1} [inst : Field K] [PerfectField K] (p : ℕ) [hp : ExpChar K p], PerfectRing K p
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.zeroLocus_inf : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (I J : Ideal A),
  ProjectiveSpectrum.zeroLocus 𝒜 ↑(I ⊓ J) = ProjectiveSpectrum.zeroLocus 𝒜 ↑I ∪ ProjectiveSpectrum.zeroLocus 𝒜 ↑J
-- Init.Data.String.Basic
String.Pos.offset_ofSliceTo : ∀ {s : String} {p₀ : s.Pos} {pos : (s.sliceTo p₀).Pos}, (String.Pos.ofSliceTo pos).offset = pos.offset
-- Mathlib.Topology.Constructions.SumProd
Filter.Tendsto.fst_nhds : ∀ {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace Z] {X : Type u_5} {l : Filter X}
  {f : X → Y × Z} {p : Y × Z}, Filter.Tendsto f l (nhds p) → Filter.Tendsto (fun a => (f a).1) l (nhds p.1)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isEmpty_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.toList.isEmpty = t.isEmpty
-- Init.Prelude
/-- Proof by cases on an `Or`. If `a ∨ b`, and both `a` and `b` imply
proposition `c`, then `c` is true.
 -/
Or.elim : ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c
-- Mathlib.Topology.MetricSpace.Similarity
Similar.comp_isometry_left_iff : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {P₃ : Type u_5} {v₁ : ι → P₁} {v₂ : ι → P₂}
  [inst : PseudoEMetricSpace P₁] [inst_1 : PseudoEMetricSpace P₂] [inst_2 : PseudoEMetricSpace P₃] {f : P₁ → P₃},
  Isometry f → (Similar (f ∘ v₁) v₂ ↔ Similar v₁ v₂)
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- Expression of `tensorIteratedFDerivTwo` in terms of `iteratedFDerivWithin`.
 -/
tensorIteratedFDerivWithinTwo_eq_iteratedFDerivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {e : E}
  {s : Set E} (f : E → F),
  UniqueDiffOn 𝕜 s →
    e ∈ s →
      ∀ (e₁ e₂ : E), (tensorIteratedFDerivWithinTwo 𝕜 f s e) (e₁ ⊗ₜ[𝕜] e₂) = (iteratedFDerivWithin 𝕜 2 f s e) ![e₁, e₂]
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.eraseTR.go.eq_2 : ∀ {α : Type u_1} [inst : BEq α] (l : List α) (a : α) (a_1 : Array α) (a_1_1 : α) (as : List α),
  List.eraseTR.go✝ l a (a_1_1 :: as) a_1 =
    bif a_1_1 == a then a_1.toListAppend as else List.eraseTR.go✝ l a as (a_1.push a_1_1)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- A costructured arrow category on a `CostructuredArrow.pre F G e` functor is equivalent to the
costructured arrow category on F  -/
CategoryTheory.CostructuredArrow.preEquivalence : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (F : CategoryTheory.Functor C D) →
              {G : CategoryTheory.Functor D E} →
                {e : E} →
                  (f : CategoryTheory.CostructuredArrow G e) →
                    CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.pre F G e) f ≌
                      CategoryTheory.CostructuredArrow F f.left
-- Mathlib.Analysis.Calculus.Deriv.Basic
derivWithin_one : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (s : Set 𝕜) [inst_3 : One F], derivWithin 1 s = 0
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.evaluation₁_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Square C} (φ : X ⟶ Y),
  CategoryTheory.Square.evaluation₁.map φ = φ.τ₁
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.setLIntegral_compProd_univ_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ]
  (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {f : β × γ → ENNReal},
  Measurable f →
    ∀ {t : Set γ},
      MeasurableSet t →
        ∫⁻ (z : β × γ) in Set.univ ×ˢ t, f z ∂(κ.compProd η) a = ∫⁻ (x : β), ∫⁻ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
/-- Given two commutative squares
```
a --φ--> b --ψ--> c
|        |        |
v        v        v
R --f--> S --g--> T
```
such that `φ ≫ ψ` and `ψ` are strongly Cartesian, then so is `φ`.  -/
CategoryTheory.Functor.IsStronglyCartesian.of_comp : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S T : 𝒮} {a b c : 𝒳} {f : R ⟶ S} {g : S ⟶ T} {φ : a ⟶ b} {ψ : b ⟶ c}
  [p.IsStronglyCartesian g ψ]
  [p.IsStronglyCartesian (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp φ ψ)]
  [p.IsHomLift f φ], p.IsStronglyCartesian f φ
-- Lean.Parser.Term
/-- A literal of type `Name`.  -/
Lean.Parser.Term.quotedName : Lean.Parser.Parser
-- Mathlib.Computability.RegularExpressions
RegularExpression.star : {α : Type u} → RegularExpression α → RegularExpression α
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instFromJsonPublishDiagnosticsParams.fromJson : Lean.Json → Except String Lean.Lsp.PublishDiagnosticsParams
-- Mathlib.Logic.Encodable.Basic
Encodable.encode_false : Encodable.encode false = 0
-- Std.Time.Zoned.Database.TzIf
/-- The count of standard/wall indicators in the file.
 -/
Std.Time.TimeZone.TZif.Header.isstdcnt : Std.Time.TimeZone.TZif.Header → UInt32
-- Init.Prelude
/-- The `>>=` operator is overloaded via instances of `bind`.

`Bind` is typically used via `Monad`, which extends it.
 -/
Bind : (Type u → Type v) → Type (max (u + 1) v)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imJ_swapEquiv_symm_apply : ∀ {R : Type u_3} (c₁ c₃ : R) [inst : CommRing R] (t : QuaternionAlgebra R c₃ 0 c₁),
  ((QuaternionAlgebra.swapEquiv c₁ c₃).symm t).imJ = t.imI
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.sInf_empty : sInf ∅ = 0
-- Mathlib.Analysis.Real.Pi.Wallis
Real.Wallis.W_eq_factorial_ratio : ∀ (n : ℕ), Real.Wallis.W n = 2 ^ (4 * n) * ↑n.factorial ^ 4 / (↑(2 * n).factorial ^ 2 * (2 * ↑n + 1))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.toList_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → t₁.toList = t₂.toList
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_rightUnitor_hom_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 : CategoryTheory.LaxFunctor B C} (η : x ⟶ x_1) (a : B),
  (CategoryTheory.Bicategory.rightUnitor η).hom.as.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).hom
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.mod_one : ∀ {R : Type u} [inst : EuclideanDomain R] (a : R), a % 1 = 0
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
cthickening_closedBall : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ ε : ℝ},
  0 ≤ ε → 0 ≤ δ → ∀ (x : E), Metric.cthickening ε (Metric.closedBall x δ) = Metric.closedBall x (ε + δ)
-- Mathlib.RingTheory.Perfection
Perfection.coeffMonoidHom_powMonoidHom : ∀ {M : Type u_1} [inst : CommMonoid M] {p : ℕ} (f : Perfection M p) (n : ℕ),
  (Perfection.coeffMonoidHom M p (n + 1)) ((powMonoidHom p) f) = (Perfection.coeffMonoidHom M p n) f
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.coe_comp_expOrderIso : Subtype.val ∘ ⇑Real.expOrderIso = Real.exp
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.restrictScalarsCLM_apply : ∀ {𝕜 : 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 : ContinuousSMul 𝕜 E] (𝕜' : Type u_5)
  [inst_9 : NontriviallyNormedField 𝕜'] [inst_10 : NormedAlgebra 𝕜' 𝕜] [inst_11 : Module 𝕜' E]
  [inst_12 : IsScalarTower 𝕜' 𝕜 E] [inst_13 : Module 𝕜' F] [inst_14 : IsScalarTower 𝕜' 𝕜 F]
  [inst_15 : ContinuousConstSMul 𝕜' F],
  ⇑(ContinuousAlternatingMap.restrictScalarsCLM 𝕜') = ContinuousAlternatingMap.restrictScalars 𝕜'
-- Mathlib.LinearAlgebra.RootSystem.WeylGroup
RootPairing.weylGroup.ofIdx_smul : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [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) (i : ι) (m : M),
  RootPairing.weylGroup.ofIdx P i • m = RootPairing.Equiv.reflection P i • m
-- Mathlib.Algebra.Module.SpanRank
/-- Generating elements for the submodule of minimum cardinality.  -/
Submodule.generators : {R : Type u_1} →
  {M : Type u} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Submodule R M → Set M
-- Mathlib.Algebra.Homology.Monoidal
HomologicalComplex.instHasTensorTensorUnit : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : (CategoryTheory.MonoidalCategory.curriedTensor C).Additive]
  [inst_5 : ∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] {I : Type u_2}
  [inst_6 : AddMonoid I] {c : ComplexShape I} [inst_7 : c.TensorSigns] (K : HomologicalComplex C c)
  [inst_8 : DecidableEq I]
  [∀ (X₂ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)],
  (HomologicalComplex.tensorUnit C c).HasTensor K
-- Mathlib.Order.Minimal
setOfPred_maximal_subset : ∀ {α : Type u_2} [inst : Preorder α] (s : Set α), {x | Maximal (fun x => x ∈ s) x} ⊆ s
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.isLongestRevMatchAtChain_skipSuffixWhile : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  (s : String.Slice), String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat (s.skipSuffixWhile pat) s.endPos
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
/-- Associator for the vertical composition of lax natural transformations.  -/
CategoryTheory.Oplax.LaxTrans.associator : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H I : CategoryTheory.OplaxFunctor B C} →
          (η : F ⟶ G) →
            (θ : G ⟶ H) →
              (ι : H ⟶ I) →
                CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp η θ) ι ≅
                  CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp θ ι)
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
card_Ico_zero_add : ∀ {M : Type u_1} [inst : AddCancelCommMonoid M] [inst_1 : LinearOrder M] [IsOrderedAddMonoid M]
  [inst_3 : LocallyFiniteOrder M] [ExistsAddOfLE M] (a b : M),
  0 ≤ a → 0 ≤ b → (Finset.Ico 0 (a + b)).card = (Finset.Ico 0 a).card + (Finset.Ico 0 b).card
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- If the action is pretransitive, then the trivial blocks condition implies preprimitivity
(based condition)  -/
AddAction.IsPreprimitive.of_isTrivialBlock_base : ∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] [AddAction.IsPretransitive G X] (a : X),
  (∀ {B : Set X}, a ∈ B → AddAction.IsBlock G B → AddAction.IsTrivialBlock B) → AddAction.IsPreprimitive G X
-- Init.Data.UInt.Bitwise
UInt16.and_neg_one : ∀ {a : UInt16}, a &&& -1 = a
-- Plausible.Gen
Plausible.GenError.genError.sizeOf_spec : ∀ (a : String), sizeOf (Plausible.GenError.genError a) = 1 + sizeOf a
-- Mathlib.Order.Interval.Finset.Defs
/-- Left-open right-open interval  -/
LocallyFiniteOrder.finsetIoo : {α : Type u_1} → {inst : Preorder α} → [self : LocallyFiniteOrder α] → α → α → Finset α
-- Mathlib.Data.QPF.Multivariate.Basic
MvQPF.supp_eq_of_isUniform : ∀ {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F],
  MvQPF.IsUniform →
    ∀ {α : TypeVec.{u} n} (a : (MvQPF.P F).A) (f : ((MvQPF.P F).B a).Arrow α) (i : Fin2 n),
      MvFunctor.supp (MvQPF.abs ⟨a, f⟩) i = f i '' Set.univ
-- Mathlib.Tactic.NormNum.Core
/-- Run each registered `norm_num` extension on a typed expression `e : α`,
returning a rational number, typed expressions `n : ℤ` and `d : ℕ` for the numerator and
denominator, and a proof of `IsRat e n d` in expression form.  -/
Mathlib.Meta.NormNum.deriveRat : {u : Lean.Level} →
  {α : Q(Type u)} →
    (e : Q(«$α»)) →
      (_inst : autoParam Q(DivisionRing «$α») Mathlib.Meta.NormNum.deriveRat._auto_1) →
        Lean.MetaM (ℚ × (n : Q(ℤ)) × (d : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsRat «$e» «$n» «$d»))
-- Mathlib.Order.Compare
eq_iff_eq_of_cmp_eq_cmp : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : α} {β : Type u_3} [inst_1 : LinearOrder β] {x' y' : β},
  cmp x y = cmp x' y' → (x = y ↔ x' = y')
-- Init.Data.Array.Monadic
Array.mapM_pure : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Array α} {f : α → β},
  Array.mapM (fun x => pure (f x)) xs = pure (Array.map f xs)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `inv_lt_inv_iff`. -/
lt_of_inv_lt_inv : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a b : α} [MulRightStrictMono α],
  a⁻¹ < b⁻¹ → b < a
-- Batteries.Lean.AttributeExtra
/-- `ParametricAttributeExtra` works around a limitation of `ParametricAttribute`, which is that
definitions must be tagged in the same file that declares the definition.
This works well for definitions in lean core, but for attributes declared outside the core
this is problematic because we may want to tag declarations created before the attribute
was defined.

To resolve this, we allow a one-time exception to the rule that attributes must be applied
in the same file as the declaration: During the declaration of the attribute itself,
we can tag arbitrary other definitions, but once the attribute is declared we must tag things
in the same file as normal.
 -/
Lean.ParametricAttributeExtra : Type → Type
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_sub_ofNat : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R) (n : ℕ)
  [inst_4 : n.AtLeastTwo], ⌈a - OfNat.ofNat n⌉ = ⌈a⌉ - OfNat.ofNat n
-- Mathlib.Topology.Category.Profinite.Nobeling.Span
Profinite.NobelingProof.factors.eq_1 : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] (s : Finset I)
  (x : ↑(Profinite.NobelingProof.π C fun x => x ∈ s)),
  Profinite.NobelingProof.factors C s x =
    List.map
      (fun i =>
        if ↑x i = true then Profinite.NobelingProof.e (Profinite.NobelingProof.π C fun x => x ∈ s) i
        else 1 - Profinite.NobelingProof.e (Profinite.NobelingProof.π C fun x => x ∈ s) i)
      (s.sort fun x1 x2 => x1 ≥ x2)
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.pullSub_append : ∀ {A : Type u_1} (T : ↥(Descriptive.tree A)) (x y : List A),
  Descriptive.Tree.pullSub (Descriptive.Tree.pullSub T y) x = Descriptive.Tree.pullSub T (x ++ y)
-- Mathlib.Data.ENNReal.Inv
/-- Order isomorphism between an initial interval in `ℝ≥0∞` and an initial interval in `ℝ≥0`.  -/
ENNReal.orderIsoIicCoe : (a : NNReal) → ↑(Set.Iic ↑a) ≃o ↑(Set.Iic a)
-- Mathlib.Data.Fin.Basic
Fin.natCast_self : ∀ (n : ℕ) [inst : NeZero n], ↑n = 0
-- Mathlib.Data.ENNReal.Real
ENNReal.one_lt_ofReal : ∀ {r : ℝ}, 1 < ENNReal.ofReal r ↔ 1 < r
-- Lean.Elab.DocString
/-- A suggestion about an applicable code block  -/
Lean.Doc.CodeBlockSuggestion : Type
-- Mathlib.Algebra.LinearRecurrence
/-- `E.mkSol init`'s first `E.order` terms are `init`.  -/
LinearRecurrence.mkSol_eq_init : ∀ {R : Type u_1} [inst : CommSemiring R] (E : LinearRecurrence R) (init : Fin E.order → R) (n : Fin E.order),
  E.mkSol init ↑n = init n
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyι_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i] {Z : C} (h : L.opcycles i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ i)
      (CategoryTheory.CategoryStruct.comp (L.homologyι i) h) =
    CategoryTheory.CategoryStruct.comp (K.homologyι i)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i) h)
-- Mathlib.RingTheory.Algebraic.Integral
Transcendental.extendScalars : ∀ {R : Type u_1} (S : Type u_2) {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] {a : A},
  Transcendental R a → ∀ [Algebra.IsAlgebraic R S], Transcendental S a
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.connected_top_iff : ∀ {V : Type u}, (SimpleGraph.completeGraph V).Connected ↔ Nonempty V
-- Mathlib.NumberTheory.LSeries.RiemannZeta
HurwitzZeta.hurwitzZeta_zero : HurwitzZeta.hurwitzZeta 0 = riemannZeta
-- Mathlib.Topology.UnitInterval
unitInterval.toNNReal_continuous : Continuous unitInterval.toNNReal
-- Mathlib.Data.List.AList
AList.mk.congr_simp : ∀ {α : Type u} {β : α → Type v} (entries entries_1 : List (Sigma β)) (e_entries : entries = entries_1)
  (nodupKeys : entries.NodupKeys),
  { entries := entries, nodupKeys := nodupKeys } = { entries := entries_1, nodupKeys := ⋯ }
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.r_iff_exists : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {x y : M × ↥S},
  (AddLocalization.r S) x y ↔ ∃ c, ↑c + (↑y.2 + x.1) = ↑c + (↑x.2 + y.1)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.toPoly.go.induct : ∀ (motive : ℕ → Nat.Internal.Linear.Expr → Prop),
  (∀ (coeff k : ℕ), (k == 0) = true → motive coeff (Nat.Internal.Linear.Expr.num k)) →
    (∀ (coeff k : ℕ), (k == 0) = false → motive coeff (Nat.Internal.Linear.Expr.num k)) →
      (∀ (coeff : ℕ) (i : Nat.Internal.Linear.Var), motive coeff (Nat.Internal.Linear.Expr.var i)) →
        (∀ (coeff : ℕ) (a b : Nat.Internal.Linear.Expr), motive coeff a → motive coeff b → motive coeff (a.add b)) →
          (∀ (coeff k : ℕ) (a : Nat.Internal.Linear.Expr),
              (k == 0) = true → motive coeff (Nat.Internal.Linear.Expr.mulL k a)) →
            (∀ (coeff k : ℕ) (a : Nat.Internal.Linear.Expr),
                (k == 0) = false → motive (coeff * k) a → motive coeff (Nat.Internal.Linear.Expr.mulL k a)) →
              (∀ (coeff : ℕ) (a : Nat.Internal.Linear.Expr) (k : ℕ), (k == 0) = true → motive coeff (a.mulR k)) →
                (∀ (coeff : ℕ) (a : Nat.Internal.Linear.Expr) (k : ℕ),
                    (k == 0) = false → motive (coeff * k) a → motive coeff (a.mulR k)) →
                  ∀ (coeff : ℕ) (a : Nat.Internal.Linear.Expr), motive coeff a
-- Mathlib.Algebra.Order.Archimedean.Basic
exists_div_btwn : ∀ {K : Type u_4} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K} {n : ℕ},
  x < y → (y - x)⁻¹ < ↑n → ∃ z, x < ↑z / ↑n ∧ ↑z / ↑n < y
-- Mathlib.CategoryTheory.Monoidal.Transport
/-- We upgrade the equivalence of categories `e : C ≌ D` to a monoidal category
equivalence `C ≌ Transported e`.  -/
CategoryTheory.Monoidal.equivalenceTransported : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (e : C ≌ D) → C ≌ CategoryTheory.Monoidal.Transported e
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_filter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool} {k : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.get? k = Option.filter (f k) (t.get? k)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preAleph_add_one : ∀ (o : Ordinal.{u_1}), Cardinal.preAleph (o + 1) = Order.succ (Cardinal.preAleph o)
-- Mathlib.Data.Set.SMulAntidiagonal
Set.VAddAntidiagonal.eq_of_snd_eq_snd : ∀ {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} {a : P} [inst : VAdd G P] {x y : ↑(s.vaddAntidiagonal t a)}
  [IsCancelVAdd G P], (↑x).2 = (↑y).2 → x = y
-- Std.Data.HashSet.Lemmas
Std.HashSet.forM_eq_forM_toList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {m' : Type v → Type w} [inst : Monad m']
  [LawfulMonad m'] {f : α → m' PUnit.{v + 1}}, forM m f = forM m.toList f