mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.iSup_add_one : ∀ {β : Type u_3} [inst : LinearOrder β] [NoMaxOrder β] {f : β → Ordinal.{u}}, StrictMono f → ⨆ i, f i + 1 = ⨆ i, f i
-- Mathlib.NumberTheory.SiegelsLemma
Int.Matrix.exists_ne_zero_int_vec_norm_le' : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (A : Matrix α β ℤ),
  Fintype.card α < Fintype.card β →
    0 < Fintype.card α →
      A ≠ 0 →
        ∃ t,
          t ≠ 0 ∧
            A.mulVec t = 0 ∧
              ‖t‖ ≤ (↑(Fintype.card β) * ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))
-- Mathlib.Topology.Continuous
closure_subset_preimage_closure_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
  Continuous f → closure s ⊆ f ⁻¹' closure (f '' s)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.IsFiniteMeasureOnCompacts.lt_top_of_isCompact : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {inst : TopologicalSpace α} {μ : MeasureTheory.Measure α}
  [self : MeasureTheory.IsFiniteMeasureOnCompacts μ] ⦃K : Set α⦄, IsCompact K → μ K < ⊤
-- Mathlib.LinearAlgebra.Dual.Lemmas
Module.dual_projective : ∀ {R : Type uR} {M : Type uM} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Finite R M] [Module.Projective R M], Module.Projective R (Module.Dual R M)
-- Mathlib.RingTheory.PowerSeries.Inverse
/-- A formal power series is invertible if the constant coefficient is invertible.  -/
PowerSeries.invOfUnit : {R : Type u_1} → [inst : Ring R] → PowerSeries R → Rˣ → PowerSeries R
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- If a set of points is affinely independent, so is any subset.  -/
AffineIndependent.mono : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s t : Set P}, (AffineIndependent k fun x => ↑x) → s ⊆ t → AffineIndependent k fun x => ↑x
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleSetName.elab : Lean.Syntax → Aesop.RuleSetName
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_diff_of_contains_eq_false_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α},
        m₂.contains k = false →
          Std.DHashMap.Internal.Raw₀.Const.get! (m₁.diff m₂) k = Std.DHashMap.Internal.Raw₀.Const.get! m₁ k
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.RelStruct.copy_map : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin (n + 1)}
  (r : f.RelStruct g i) {f' g' : X.PtSimplex n x} (hf : f = f') (hg : g = g'), (r.copy hf hg).map = r.map
-- Mathlib.GroupTheory.Exponent
Monoid.exponent_eq_iSup_orderOf : ∀ {G : Type u} [inst : CommMonoid G], (∀ (g : G), 0 < orderOf g) → Monoid.exponent G = ⨆ g, orderOf g
-- Mathlib.Analysis.Calculus.FDeriv.Add
differentiableAt_add_const_iff : ∀ {𝕜 : 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] {f : E → F}
  {x : E} (c : F), DifferentiableAt 𝕜 (fun y => f y + c) x ↔ DifferentiableAt 𝕜 f x
-- Mathlib.Algebra.Module.NatInt
AddCommGroup.toIntModule : (M : Type u_3) → [inst : AddCommGroup M] → Module ℤ M
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- A reformulation of `IsCyclotomicExtension` that uses `⊤`.  -/
IsCyclotomicExtension.iff_adjoin_eq_top : ∀ (S : Set ℕ) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
  IsCyclotomicExtension S A B ↔
    (∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n) ∧ Algebra.adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} = ⊤
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.forget_reflects_isos : (CategoryTheory.forget AddMonCat).ReflectsIsomorphisms
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.isOpen : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s : TopologicalSpace.Clopens α), IsOpen ↑s
-- Init.Data.SInt.Bitwise
ISize.toBitVec_abs : ∀ (a : ISize), a.abs.toBitVec = a.toBitVec.abs
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
ZMod.toCircle.congr_simp : ∀ {N : ℕ} [inst : NeZero N], ZMod.toCircle = ZMod.toCircle
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.instReprSimpCongrTheorem.repr : Lean.Meta.SimpCongrTheorem → ℕ → Std.Format
-- Lean.Elab.Tactic.Omega.Core
/-- A `omega` problem.

This is a hybrid structure:
it contains both `Expr` objects giving proofs of the "ground" assumptions
(or rather continuations which will produce the proofs when needed)
and internal representations of the linear constraints that we manipulate in the algorithm.

While the algorithm is running we do not synthesize any new `Expr` proofs: proof extraction happens
only once we've found a contradiction.
 -/
Lean.Elab.Tactic.Omega.Problem : Type
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.uniqueHomFromTrivial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (A : CategoryTheory.Grp C) → Unique (CategoryTheory.Grp.trivial C ⟶ A)
-- Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
MonoidAlgebra.smul_apply_mulAction : ∀ {G : Type u_1} {P : Type u_2} {R : Type u_3} {V : Type u_4} [inst : Group G] [inst_1 : MulAction G P]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid V] [inst_4 : SMulWithZero R V] (f : MonoidAlgebra R G) (x : P → V)
  (p : P), (f • x) p = ∑ i ∈ f.coeff.support, f.coeff i • x (i⁻¹ • p)
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.isStableUnderCoproductsOfShape_cofibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)] (J : Type w),
  (HomotopicalAlgebra.cofibrations C).IsStableUnderCoproductsOfShape J
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.instIsScalarTower : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] (S : NonUnitalStarSubalgebra R A) [IsScalarTower R A A], IsScalarTower R ↥S ↥S
-- Init.Data.Array.Erase
Array.exists_of_eraseP : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α} {a : α},
  a ∈ xs → p a = true → ∃ a ys zs, (∀ b ∈ ys, ¬p b = true) ∧ p a = true ∧ xs = ys.push a ++ zs ∧ xs.eraseP p = ys ++ zs
-- Mathlib.LinearAlgebra.Basis.VectorSpace
LinearMap.leftInverse.eq_1 : ∀ {K : Type u_3} {V : Type u_4} {V' : Type u_5} [inst : DivisionRing K] [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup V'] [inst_3 : Module K V] [inst_4 : Module K V'] (f : V →ₗ[K] V'),
  f.leftInverse = if h_inj : f.ker = ⊥ then ⋯.choose else 0
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.openCell_subset_skeleton`. -/
Topology.CWComplex.openCell_subset_skeleton : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] (n : ℕ)
  (j : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.openCell n j ⊆ ↑(Topology.RelCWComplex.skeleton C ↑n)
-- Mathlib.Topology.Spectral.Hom
SpectralMap.mk : {α : Type u_6} →
  {β : Type u_7} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → (toFun : α → β) → IsSpectralMap toFun → SpectralMap α β
-- Mathlib.Order.CompleteBooleanAlgebra
CompletelyDistribLattice.toHImp : {α : Type u} → [self : CompletelyDistribLattice α] → HImp α
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netEntropyEntourage_univ : ∀ {X : Type u_1} (T : X → X) {F : Set X}, F.Nonempty → Dynamics.netEntropyEntourage T F Set.univ = 0
-- Mathlib.Topology.Sheaves.Over
TopologicalSpace.Opens.instIsDenseSubsiteSubtypeMemOverGrothendieckTopologyOverInverseOverEquivalence : ∀ {X : Type u} [inst : TopologicalSpace X] (U : TopologicalSpace.Opens X),
  CategoryTheory.Functor.IsDenseSubsite (Opens.grothendieckTopology ↥U) ((Opens.grothendieckTopology X).over U)
    U.overEquivalence.inverse
-- Mathlib.Combinatorics.Graph.Basic
/-- The binary incidence predicate can be expressed in terms of the unary one.  -/
Graph.isLink_iff_inc : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β},
  G.IsLink e x y ↔ G.Inc e x ∧ G.Inc e y ∧ ∀ (z : α), G.Inc e z → z = x ∨ z = y
-- Mathlib.GroupTheory.Transfer
MonoidHom.transfer.congr_simp : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {A : Type u_2} [inst_1 : CommGroup A] (ϕ ϕ_1 : ↥H →* A),
  ϕ = ϕ_1 → ∀ [inst_2 : H.FiniteIndex], ϕ.transfer = ϕ_1.transfer
-- Lean.Elab.ParseImportsFast
Lean.instToJsonPrintImportsResult : Lean.ToJson Lean.PrintImportsResult
-- Mathlib.Data.Finset.NAry
Finset.image₂_subset : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s s' : Finset α}
  {t t' : Finset β}, s ⊆ s' → t ⊆ t' → Finset.image₂ f s t ⊆ Finset.image₂ f s' t'
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
/-- `P.Under.pushout` is left adjoint to `P.Under.map` if pushouts of morphisms satisfying `P`
exist along `f` and are also in `P`, and `f` is in both `P` and `Q`.  -/
CategoryTheory.MorphismProperty.Under.mapPushoutAdj : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    (P Q : CategoryTheory.MorphismProperty T) →
      [inst_1 : Q.IsMultiplicative] →
        {X Y : T} →
          [inst_2 : P.IsStableUnderComposition] →
            [inst_3 : Q.IsStableUnderCobaseChange] →
              (f : X ⟶ Y) →
                [inst_4 : P.HasPushoutsAlong f] →
                  [inst_5 : P.IsStableUnderCobaseChangeAlong f] →
                    [Q.HasOfPrecompProperty Q] →
                      (hPf : P f) →
                        Q f →
                          (CategoryTheory.MorphismProperty.Under.pushout P Q f ⊣
                            CategoryTheory.MorphismProperty.Under.map Q hPf)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.instZSMul : {R : Type u} → [inst : Ring R] → SMul ℤ (Polynomial R)
-- Mathlib.Algebra.Order.Group.Synonym
toColex_add : ∀ {α : Type u_1} [inst : Add α] (a b : α), toColex (a + b) = toColex a + toColex b
-- Batteries.CodeAction.Attr
/-- The tactic kinds that this extension supports. If empty it is called on all tactic kinds.  -/
Batteries.CodeAction.TacticCodeActionEntry.tacticKinds : Batteries.CodeAction.TacticCodeActionEntry → Array Lean.Name
-- Mathlib.MeasureTheory.Covering.Besicovitch
HasBesicovitchCovering.mk : ∀ {α : Type u_1} [inst : MetricSpace α],
  (∃ N τ, 1 < τ ∧ IsEmpty (Besicovitch.SatelliteConfig α N τ)) → HasBesicovitchCovering α
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.map_Q₁ : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥),
  Polynomial.map (algebraMap (Polynomial K) (RatFunc K)) (RatFunc.Luroth.Q₁✝ h) = RatFunc.Luroth.Q₀✝ E
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
/-- The expression for the underlying category.  -/
Mathlib.Tactic.Monoidal.Context.C : (self : Mathlib.Tactic.Monoidal.Context) → Q(Type udummy._pp_uniq.3)
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.integrable_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  [inst_3 : NormedAddCommGroup γ] [BorelSpace γ],
  ProbabilityTheory.IdentDistrib f g μ ν → (MeasureTheory.Integrable f μ ↔ MeasureTheory.Integrable g ν)
-- Std.Time.Zoned.Database.TzIf
_private.Std.Time.Zoned.Database.TzIf.0.Std.Time.TimeZone.TZif.toInt64 : ByteArray → ℤ
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Over.coprodObj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C] {A : C}
  (a : CategoryTheory.Over A) {X Y : CategoryTheory.Over A} (k : X ⟶ Y),
  a.coprodObj.map k =
    CategoryTheory.Over.homMk
      (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id a.left) (CategoryTheory.Over.Hom.left k)) ⋯
-- Mathlib.Algebra.Order.IsBotOne
max_one : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : One α] [IsBotOneClass α] (a : α), max a 1 = a
-- Lean.Language.Basic
/-- Synchronously waits on the result of the task.  -/
Lean.Language.SnapshotTask.get : {α : Type} → Lean.Language.SnapshotTask α → α
-- Mathlib.Analysis.Complex.Exponential
Real.exp_1_approx_succ_eq : ∀ {n : ℕ} {a₁ b₁ : ℝ} {m : ℕ},
  n + 1 = m →
    ∀ {rm : ℝ},
      ↑m = rm →
        |Real.exp 1 - Real.expNear m 1 ((a₁ - 1) * rm)| ≤ |1| ^ m / ↑m.factorial * (b₁ * rm) →
          |Real.exp 1 - Real.expNear n 1 a₁| ≤ |1| ^ n / ↑n.factorial * b₁
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.insertMax.congr_simp : ∀ {α : Type u} {β : α → Type v} (k : α) (v v_1 : β k),
  v = v_1 →
    ∀ (t : Std.DTreeMap.Internal.Impl α β) (hl : t.Balanced),
      Std.DTreeMap.Internal.Impl.insertMax k v t hl = Std.DTreeMap.Internal.Impl.insertMax k v_1 t hl
-- Aesop.Forward.LevelIndex
Aesop.LevelIndex.mk.injEq : ∀ (toNat toNat_1 : ℕ), ({ toNat := toNat } = { toNat := toNat_1 }) = (toNat = toNat_1)
-- Mathlib.Algebra.Ring.Action.End
RingAut.smul_def : ∀ {R : Type u_2} [inst : Semiring R] (f : RingAut R) (r : R), f • r = f r
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instBEqLetValue : {pu : Lean.Compiler.LCNF.Purity} → BEq (Lean.Compiler.LCNF.LetValue pu)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₂ → (t₁ \ t₂).getKey? k = none
-- Mathlib.Topology.Sheaves.Over
TopologicalSpace.Opens.mem_overEquivalence_functor_obj : ∀ {X : Type u} [inst : TopologicalSpace X] {U : TopologicalSpace.Opens X} {V : CategoryTheory.Over U} {x : ↥U},
  x ∈ U.overEquivalence.functor.obj V ↔ ↑x ∈ V.left
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.d₂_eq_zero' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁ : I₁) {i₂ i₂' : I₂}, c₂.Rel i₂ i₂' → ∀ (i₁₂ : I₁₂), c₁.π c₂ c₁₂ (i₁, i₂') ≠ i₁₂ → K.d₂ c₁₂ i₁ i₂ i₁₂ = 0
-- Mathlib.RingTheory.Localization.Cardinality
Cardinal.mk_fractionRing : ∀ (R : Type u) [inst : CommRing R], Cardinal.mk (FractionRing R) = Cardinal.mk R
-- Mathlib.RingTheory.Ideal.Operations
/-- An element `x` lies in the span of `v` iff it can be written as sum `∑ cᵢ • vᵢ = x`.
 -/
Ideal.mem_span_range_iff_exists_fun : ∀ {α : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : Fintype α] {x : R} {v : α → R},
  x ∈ Ideal.span (Set.range v) ↔ ∃ c, ∑ i, c i * v i = x
-- Lean.Setup
Lean.ImportArtifacts.ofArrays.inj : ∀ {toArrays toArrays_1 : Array (Array System.FilePath)},
  { toArrays := toArrays } = { toArrays := toArrays_1 } → toArrays = toArrays_1
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.Code.forM.go : {m : Type → Type u_1} →
  {pu : Lean.Compiler.LCNF.Purity} →
    [Monad m] → (Lean.Compiler.LCNF.Code pu → m Unit) → Lean.Compiler.LCNF.Code pu → m Unit
-- Mathlib.RingTheory.Length
Module.length_ne_top_iff_finiteDimensionalOrder : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.length R M ≠ ⊤ ↔ FiniteDimensionalOrder (Submodule R M)
-- Mathlib.NumberTheory.LucasLehmer
mersenne.eq_1 : ∀ (p : ℕ), mersenne p = 2 ^ p - 1
-- Mathlib.Algebra.Group.Equiv.Opposite
MulHom.op_apply_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (a : Mᵐᵒᵖ),
  (MulHom.op f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a
-- Mathlib.Analysis.Matrix.LDL
LDL.diagEntries.congr_simp : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : LinearOrder n] [inst_2 : WellFoundedLT n]
  [inst_3 : LocallyFiniteOrderBot n] {S S_1 : Matrix n n 𝕜} (e_S : S = S_1) [inst_4 : Fintype n] (hS : S.PosDef)
  (a a_1 : n), a = a_1 → LDL.diagEntries hS a = LDL.diagEntries ⋯ a_1
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.le_infDist : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α} {r : ℝ},
  s.Nonempty → (r ≤ Metric.infDist x s ↔ ∀ ⦃y : α⦄, y ∈ s → r ≤ dist x y)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPushforward_equivalence_eq_pullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {U : C} (S : CategoryTheory.Sieve U),
  CategoryTheory.Sieve.functorPushforward e.inverse (CategoryTheory.Sieve.functorPushforward e.functor S) =
    CategoryTheory.Sieve.pullback (e.unitInv.app U) S
-- Mathlib.GroupTheory.GroupAction.Period
AddAction.period_neg : ∀ {α : Type v} {G : Type u} [inst : AddGroup G] [inst_1 : AddAction G α] (g : G) (a : α),
  AddAction.period (-g) a = AddAction.period g a
-- Mathlib.Algebra.Module.ULift
ULift.mulActionWithZero' : {R : Type u} →
  {M : Type v} →
    [inst : MonoidWithZero R] → [inst_1 : Zero M] → [MulActionWithZero R M] → MulActionWithZero R (ULift.{u_1, v} M)
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- If distinct points `p₁` and `p₃` lie in `s` but `p₂` does not, the three points are affinely
independent.  -/
affineIndependent_of_ne_of_mem_of_notMem_of_mem : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p₁ p₂ p₃ : P},
  p₁ ≠ p₃ → p₁ ∈ s → p₂ ∉ s → p₃ ∈ s → AffineIndependent k ![p₁, p₂, p₃]
-- Mathlib.Algebra.Homology.Bifunctor
CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_map_f_f : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  {I₁ : Type u_4} {I₂ : Type u_5} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (K₁ : HomologicalComplex C₁ c₁)
  {K₂ K₂' : HomologicalComplex C₂ c₂} {φ : K₂ ⟶ K₂'} (i₁ : I₁) (i₂ : I₂),
  ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).map φ).f i₁).f i₂ = (F.obj (K₁.X i₁)).map (φ.f i₂)
-- Mathlib.LinearAlgebra.Matrix.IsDiag
/-- Every identity matrix is diagonal.  -/
Matrix.isDiag_one : ∀ {α : Type u_1} {n : Type u_4} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α], Matrix.IsDiag 1
-- Lean.DocString.Markdown
/-- A run of `` ` `` characters one longer than any run inside `str` (with a minimum of `atLeast`),
suitable for use as a code block fence or a delimiter for inline code.
 -/
_private.Lean.DocString.Markdown.0.Lean.Doc.fenceFor : ℕ → String → String
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- **Alias** of the reverse direction of `Subalgebra.finiteDimensional_toSubmodule`.

---

A `Subalgebra` is `FiniteDimensional` iff it is `FiniteDimensional` as a submodule.  -/
FiniteDimensional.subalgebra_toSubmodule : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Ring E] [inst_2 : Algebra F E] {S : Subalgebra F E},
  FiniteDimensional F ↥S → FiniteDimensional F ↥(Subalgebra.toSubmodule S)
-- Mathlib.Data.Analysis.Topology
Ctop.Realizer.F : {α : Type u_6} → [T : TopologicalSpace α] → (self : Ctop.Realizer α) → Ctop α self.σ
-- Std.Data.String.ToInt
String.Slice.toInt?_eq_of_eq_minus_append : ∀ {s : String.Slice} {t : String}, s.copy = "-" ++ t → s.toInt? = Option.map (fun n => -↑n) t.toNat?
-- Mathlib.Topology.Connected.Clopen
ConnectedComponents.nonempty_iff_nonempty : ∀ {α : Type u} [inst : TopologicalSpace α], Nonempty (ConnectedComponents α) ↔ Nonempty α
-- Lean.Data.Json.FromToJson.Basic
Lean.instToJsonInt : Lean.ToJson ℤ
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min!_le_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k : α}, t.contains k = true → (cmp t.min! k).isLE = true
-- Mathlib.Topology.Convenient.GeneratedBy
Topology.IsGeneratedBy.equiv_symm_comp_continuous_iff : ∀ {ι : Type t} (X : ι → Type u) [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  {Z : Type v'} [inst_1 : TopologicalSpace Z] [Topology.IsGeneratedBy X Y] (g : Y → Z),
  Continuous (⇑Topology.WithGeneratedByTopology.equiv.symm ∘ g) ↔ Continuous g
-- Mathlib.Algebra.Regular.Basic
IsAddRegular.nsmul_iff : ∀ {R : Type u_1} [inst : AddMonoid R] {a : R} {n : ℕ}, 0 < n → (IsAddRegular (n • a) ↔ IsAddRegular a)
-- Mathlib.RingTheory.MvPolynomial
MvPolynomial.rank_eq : ∀ {K : Type v} [inst : CommRing K] [Nontrivial K] {σ : Type v}, Module.rank K (MvPolynomial σ K) = Cardinal.mk (σ →₀ ℕ)
-- Mathlib.Topology.Covering.Basic
IsCoveringMap.const_of_comp : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X},
  IsCoveringMap f →
    ∀ {A : Type u_3} [inst_2 : TopologicalSpace A] {g : A → E} [PreconnectedSpace A],
      Continuous g → (∀ (a a' : A), f (g a) = f (g a')) → ∀ (a a' : A), g a = g a'
-- Mathlib.Tactic.Check
/-- The `#check'` command is like `#check`, but only prints explicit arguments in the signature
(i.e., omitting implicit and typeclass arguments).  -/
Mathlib.Tactic.«command#check'_» : Lean.ParserDescr
-- Lean.Data.Options
Lean.Options.mergeBy : (Lean.Name → Lean.DataValue → Lean.DataValue → Lean.DataValue) → Lean.Options → Lean.Options → Lean.Options
-- Mathlib.Data.Multiset.Defs
/-- **Alias** of `Multiset.subset_of_le`. -/
Multiset.Le.subset : ∀ {α : Type u_1} {s t : Multiset α}, s ≤ t → s ⊆ t
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.symm_trans_cancel_left : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [inst_6 : RingHomInvPair σ₁₃ σ₃₁]
  [inst_7 : RingHomInvPair σ₃₁ σ₁₃] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃}
  [inst_8 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_9 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
  [inst_10 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃] [inst_11 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂] (e : M₁ ≃ₛₗ[σ₁₂] M₂)
  (f : M₂ ≃ₛₗ[σ₂₃] M₃), e.symm.trans (e.trans f) = f
-- Mathlib.Analysis.Convex.Deriv
/-- If `f : ℝ → ℝ` is strictly convex on `S` and differentiable at `y ∈ S`, then the slope of any
secant line with right endpoint at `y` is strictly less than the derivative of `f` at `y`.  -/
StrictConvexOn.slope_lt_of_hasDerivAt : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ},
  StrictConvexOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivAt f f' y → slope f x y < f'
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.Context.sctx : Lean.Elab.Tactic.Grind.Context → Lean.Meta.Sym.Context
-- Mathlib.Algebra.MvPolynomial.Derivation
MvPolynomial.mkDerivationₗ_C : ∀ {σ : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Module (MvPolynomial σ R) A] (f : σ → A) (r : R), (MvPolynomial.mkDerivationₗ R f) (MvPolynomial.C r) = 0
-- Batteries.Util.Cache
/-- Wraps the given action for use in `EIO.asTask` etc., discarding its final monadic state.  -/
Lean.Meta.wrapAsync : {β α : Type} → (α → Lean.MetaM β) → Option IO.CancelToken → Lean.MetaM (α → EIO Lean.Exception β)