mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Graded
GradedLieAlgebra.mk : {ι : Type u_1} →
  {R : Type u_3} →
    {L : Type u_4} →
      [inst : DecidableEq ι] →
        [inst_1 : AddCommMonoid ι] →
          [inst_2 : CommRing R] →
            [inst_3 : LieRing L] →
              [inst_4 : LieAlgebra R L] →
                {ℒ : ι → Submodule R L} →
                  [toGradedBracket : SetLike.GradedBracket ℒ] →
                    [toDecomposition : DirectSum.Decomposition ℒ] → GradedLieAlgebra ℒ
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.evalCases : Lean.Elab.Tactic.Tactic
-- Mathlib.Data.Sum.Order
/-- `Equiv.sumCongr` promoted to an order isomorphism.  -/
OrderIso.sumCongr : {α₁ : Type u_4} →
  {α₂ : Type u_5} →
    {β₁ : Type u_6} →
      {β₂ : Type u_7} →
        [inst : LE α₁] →
          [inst_1 : LE α₂] → [inst_2 : LE β₁] → [inst_3 : LE β₂] → α₁ ≃o α₂ → β₁ ≃o β₂ → α₁ ⊕ β₁ ≃o α₂ ⊕ β₂
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileSystemWatcher.globPattern : Lean.Lsp.FileSystemWatcher → String
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instSub : {R : Type u_3} → {A : Type u_4} → [Sub R] → [Sub A] → Sub (Unitization R A)
-- Batteries.Data.List.Basic
/-- `Forall₂ R l₁ l₂` means that `l₁` and `l₂` have the same length,
and whenever `a` is the nth element of `l₁`, and `b` is the nth element of `l₂`,
then `R a b` is satisfied.
 -/
List.Forall₂ : {α : Type u_1} → {β : Type u_2} → (α → β → Prop) → List α → List β → Prop
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.coverEntropyEntourage_union : ∀ {X : Type u_1} {T : X → X} {F G : Set X} {U : SetRel X X},
  Dynamics.coverEntropyEntourage T (F ∪ G) U =
    max (Dynamics.coverEntropyEntourage T F U) (Dynamics.coverEntropyEntourage T G U)
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.EntriesNode : Type u_1 → Type u_2 → Type (max 0 u_2 u_1)
-- Mathlib.Data.NNReal.Defs
NNReal.coe_inj : ∀ {r₁ r₂ : NNReal}, ↑r₁ = ↑r₂ ↔ r₁ = r₂
-- Mathlib.NumberTheory.WellApproximable
wellApproximable.eq_1 : ∀ (A : Type u_1) [inst : SeminormedGroup A] (δ : ℕ → ℝ),
  wellApproximable A δ = Filter.blimsup (fun n => approxOrderOf A n (δ n)) Filter.atTop fun n => 0 < n
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.coeff_out : ∀ {p n : ℕ} {R : Type u_1} [inst : CommRing R] (x : TruncatedWittVector p n R) (i : Fin n),
  x.out.coeff ↑i = TruncatedWittVector.coeff i x
-- Init.GrindInstances.Ring.UInt
UInt64.natCast : NatCast UInt64
-- Mathlib.Order.Hom.Basic
/-- `Equiv.equivOfIsEmpty` promoted to an `OrderIso`.  -/
OrderIso.ofIsEmpty : (α : Type u_6) → (β : Type u_7) → [inst : Preorder α] → [inst_1 : Preorder β] → [IsEmpty α] → [IsEmpty β] → α ≃o β
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.formatMonthLong : Std.Time.DateFormatSymbols → Std.Time.Month.Ordinal → String
-- Mathlib.LinearAlgebra.Alternating.DomCoprod
/-- A more bundled version of `AlternatingMap.domCoprod` that maps
`((ι₁ → N) → N₁) ⊗ ((ι₂ → N) → N₂)` to `(ι₁ ⊕ ι₂ → N) → N₁ ⊗ N₂`.  -/
AlternatingMap.domCoprod' : {ιa : Type u_1} →
  {ιb : Type u_2} →
    [Fintype ιa] →
      [Fintype ιb] →
        {R' : Type u_3} →
          {Mᵢ : Type u_4} →
            {N₁ : Type u_5} →
              {N₂ : Type u_6} →
                [inst : CommSemiring R'] →
                  [inst_1 : AddCommGroup N₁] →
                    [inst_2 : Module R' N₁] →
                      [inst_3 : AddCommGroup N₂] →
                        [inst_4 : Module R' N₂] →
                          [inst_5 : AddCommMonoid Mᵢ] →
                            [inst_6 : Module R' Mᵢ] →
                              [DecidableEq ιa] →
                                [DecidableEq ιb] →
                                  TensorProduct R' (Mᵢ [⋀^ιa]→ₗ[R'] N₁) (Mᵢ [⋀^ιb]→ₗ[R'] N₂) →ₗ[R']
                                    Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] TensorProduct R' N₁ N₂
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.toAffineEquiv_pointReflection : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁] [inst_5 : TopologicalSpace V₁]
  [inst_6 : IsTopologicalAddTorsor P₁] (x : P₁),
  ↑(ContinuousAffineEquiv.pointReflection k x) = AffineEquiv.pointReflection k x
-- Mathlib.Topology.Connected.Clopen
ConnectedComponents.isQuotientMap_coe : ∀ {α : Type u} [inst : TopologicalSpace α], Topology.IsQuotientMap ConnectedComponents.mk
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHomClass.mk : ∀ {F : Type u_6} {α : outParam (Type u_7)} [inst : NonUnitalNonAssocSemiring α] [inst_1 : FunLike F α α]
  [toAddMonoidHomClass : AddMonoidHomClass F α α],
  (∀ (f : F) (a b : α), f (a * b) = a * f b) → (∀ (f : F) (a b : α), f (a * b) = f a * b) → CentroidHomClass F α
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_le_toNNReal : ∀ {r p : ℝ}, r ≤ p → r.toNNReal ≤ p.toNNReal
-- Mathlib.GroupTheory.CoprodI
freeGroupEquivCoprodI_apply : ∀ {ι : Type u_1} (a : FreeGroup ι),
  freeGroupEquivCoprodI a = (FreeGroup.lift fun i => Monoid.CoprodI.of (FreeGroup.of ())) a
-- Mathlib.Tactic.NormNum.Ineq
/-- Helper function to synthesize typed `Semifield α` `LinearOrder α` `IsStrictOrderedRing α`
expressions.  -/
Mathlib.Meta.NormNum.inferLinearOrderedSemifield : {u : Lean.Level} →
  (α : Q(Type u)) → Lean.MetaM ((x : Q(Semifield «$α»)) × (x_1 : Q(LinearOrder «$α»)) × Q(IsStrictOrderedRing «$α»))
-- Init.Prelude
instNonemptyOfMonad : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [Nonempty α], Nonempty (m α)
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.adjoin_root_eq_top : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f), R[h.root] = ⊤
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsBigOTVS.trans : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] [inst_7 : AddCommGroup G] [inst_8 : TopologicalSpace G]
  [inst_9 : Module 𝕜 G] {l : Filter α} {f : α → E} {g : α → F} {k : α → G}, f =O[𝕜; l] g → g =O[𝕜; l] k → f =O[𝕜; l] k
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_le_of_le_of_le : ∀ {ι : Type u_1} (s : Finset ι) [inst : (j : ι) → Decidable (j ∈ s)] {π : ι → Type u_3} {f g h : (i : ι) → π i}
  [inst_1 : (i : ι) → Preorder (π i)], f ≤ h → g ≤ h → s.piecewise f g ≤ h
-- Mathlib.Analysis.Calculus.Deriv.ZPow
iter_deriv_zpow' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (m : ℤ) (k : ℕ),
  (deriv^[k] fun x => x ^ m) = fun x => (∏ i ∈ Finset.range k, (↑m - ↑i)) * x ^ (m - ↑k)
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
addMonoidAlgebraAddEquivDirectSum_apply_toFun : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring M] [inst_2 : (m : M) → Decidable (m ≠ 0)]
  (f : AddMonoidAlgebra M ι), ⇑(addMonoidAlgebraAddEquivDirectSum f) = ⇑f.coeff
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.instContinuousVAddCoePrincipal : ∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  {T : Set ι} [inst_1 : (i : ι) → TopologicalSpace (R i)] {G : Type u_4} [inst_2 : TopologicalSpace G]
  [inst_3 : (i : ι) → VAdd G (R i)] [inst_4 : ∀ (i : ι), VAddMemClass (S i) G (R i)]
  [∀ (i : ι), ContinuousVAdd G (R i)],
  ContinuousVAdd G (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) (Filter.principal T))
-- Lean.Meta.Basic
/-- When `constApprox` is set to true,
we solve `?m t =?= c` using
`?m := fun _ => c`
when `?m t` is not a higher-order pattern and `c` is not an application as  -/
Lean.Meta.Config.constApprox : Lean.Meta.Config → Bool
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.isOrtho_zero_right : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M} (x : M), B.IsOrtho x 0
-- Mathlib.Algebra.Order.GroupWithZero.Defs
MulPosStrictMono.mk : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α],
  (∀ ⦃c : α⦄, 0 < c → ∀ ⦃a b : α⦄, a < b → a * c < b * c) → MulPosStrictMono α
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.continuous_negPart : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [inst : Fact (1 ≤ p)],
  Continuous fun f => MeasureTheory.Lp.negPart f
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.mapId_inv_app_left : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) [inst_1 : Q.IsMultiplicative] [inst_2 : P.IsStableUnderComposition]
  [inst_3 : P.IsMultiplicative] [inst_4 : Q.RespectsIso] (X : T)
  (f : optParam (X ⟶ X) (CategoryTheory.CategoryStruct.id X))
  (hf : autoParam (f = CategoryTheory.CategoryStruct.id X) CategoryTheory.MorphismProperty.Over.mapId._auto_1)
  (X_1 : P.Over Q X),
  ((CategoryTheory.MorphismProperty.Over.mapId Q X f hf).inv.app X_1).left = CategoryTheory.CategoryStruct.id X_1.left
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.ncard_sdiff_singleton_lt_of_mem`. -/
Set.ncard_diff_singleton_lt_of_mem : ∀ {α : Type u_1} {s : Set α} {a : α},
  a ∈ s → autoParam s.Finite Set.ncard_sdiff_singleton_lt_of_mem._auto_1 → (s \ {a}).ncard < s.ncard
-- Mathlib.GroupTheory.Exponent
/-- The exponent of an additive submonoid `H ≤ G` divides the exponent of `G`.  -/
AddMonoid.exponent_addSubmonoid_dvd : ∀ {G : Type u} [inst : AddMonoid G] (H : AddSubmonoid G), AddMonoid.exponent ↥H ∣ AddMonoid.exponent G
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.map_sub₂ : ∀ {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {S₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : Semiring S] [inst_3 : Semiring S₂] {N : Type u_7} [inst_4 : AddCommMonoid N] [inst_5 : Module S N]
  {M' : Type u_12} {P' : Type u_13} [inst_6 : AddCommGroup M'] [inst_7 : AddCommGroup P'] [inst_8 : Module R M']
  [inst_9 : Module R₂ P'] [inst_10 : Module S₂ P'] [inst_11 : SMulCommClass S₂ R₂ P'] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂}
  (f : M' →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P') (x y : M') (z : N), (f (x - y)) z = (f x) z - (f y) z
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.instUniqueOfIsEmpty.eq_1 : ∀ {α : Type u_1} [inst : IsEmpty α],
  FreeMonoid.instUniqueOfIsEmpty = { toInhabited := FreeMonoid.instInhabited, uniq := ⋯ }
-- Mathlib.CategoryTheory.Preadditive.HomOrthogonal
CategoryTheory.HomOrthogonal.matrixDecomposition_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C}
  [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C]
  (o : CategoryTheory.HomOrthogonal s) {α : Type} [inst_3 : Finite α] {f : α → ι} (i : ι),
  o.matrixDecomposition (CategoryTheory.CategoryStruct.id (⨁ fun a => s (f a))) i = 1
-- Mathlib.Data.List.Sort
/-- Another statement of stability of insertion sort.
If a pair `[a, b]` is a sublist of a permutation of `l` and `a ≼ b`,
then `[a, b]` is still a sublist of `insertionSort r l`.
 -/
List.pair_sublist_insertionSort' : ∀ {α : Type u_1} {r : α → α → Prop} [inst : DecidableRel r] [Std.Antisymm r] [Std.Total r] [IsTrans α r] {a b : α}
  {l : List α}, r a b → [a, b].Subperm l → [a, b].Sublist (List.insertionSort r l)
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.instIsSplitEpiOppositeOpOfIsSplitMono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.IsSplitMono f],
  CategoryTheory.IsSplitEpi f.op
-- Mathlib.Probability.Kernel.IonescuTulcea.Maps
/-- Gluing `Iic a` and `Ioc a b` into `Iic b`. This version requires `a ≤ b` to get a measurable
equivalence.  -/
MeasurableEquiv.IicProdIoc : {ι : Type u_1} →
  [inst : LinearOrder ι] →
    [inst_1 : LocallyFiniteOrder ι] →
      [DecidableLE ι] →
        {X : ι → Type u_2} →
          [inst_3 : LocallyFiniteOrderBot ι] →
            [inst_4 : (i : ι) → MeasurableSpace (X i)] →
              {a b : ι} →
                a ≤ b →
                  ((i : ↥(Finset.Iic a)) → X ↑i) × ((i : ↥(Finset.Ioc a b)) → X ↑i) ≃ᵐ ((i : ↥(Finset.Iic b)) → X ↑i)
-- Lean.Elab.Binders
Lean.Elab.Term.BinderView.mk.inj : ∀ {ref id type : Lean.Syntax} {bi : Lean.BinderInfo} {ref_1 id_1 type_1 : Lean.Syntax} {bi_1 : Lean.BinderInfo},
  { ref := ref, id := id, type := type, bi := bi } = { ref := ref_1, id := id_1, type := type_1, bi := bi_1 } →
    ref = ref_1 ∧ id = id_1 ∧ type = type_1 ∧ bi = bi_1
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightId_hom_app_right : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  (L : CategoryTheory.Functor A T) (X : CategoryTheory.Comma L R),
  ((CategoryTheory.Comma.mapRightId R L).hom.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.IsMaximal.lt_top : ∀ {α : Type u} [inst : Semiring α] {I : Ideal α}, I.IsMaximal → I < ⊤
-- Mathlib.Algebra.Group.Equiv.Defs
/-- Makes a multiplicative isomorphism from a bijection which preserves multiplication.  -/
MulEquiv.mk' : {M : Type u_4} →
  {N : Type u_5} → [inst : Mul M] → [inst_1 : Mul N] → (f : M ≃ N) → (∀ (x y : M), f (x * y) = f x * f y) → M ≃* N
-- Mathlib.RingTheory.Algebraic.MvPolynomial
Set.subtypeInsertEquivOption.congr_simp : ∀ {α : Type u_1} [inst : DecidableEq α] {t : Set α} {x : α} (h : x ∉ t),
  Set.subtypeInsertEquivOption h = Set.subtypeInsertEquivOption h
-- Mathlib.Data.Matrix.PEquiv
/-- We can also define permutation matrices by permuting the rows of the identity matrix.  -/
PEquiv.toMatrix_toPEquiv_eq : ∀ {n : Type u_4} {α : Type u_5} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α] (σ : Equiv.Perm n),
  (Equiv.toPEquiv σ).toMatrix = Matrix.submatrix 1 (⇑σ) id
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.toMatrix.eq_1 : ∀ {n : Type u_1} {R : Type u₂} [inst : DecidableEq n] [inst_1 : CommRing R] (t : Matrix.TransvectionStruct n R),
  t.toMatrix = Matrix.transvection t.i t.j t.c
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Natural transformations between functors lift to monoid objects.  -/
CategoryTheory.Functor.mapMonNatTrans : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F F' : CategoryTheory.Functor C D} →
              [inst_4 : F.LaxMonoidal] →
                [inst_5 : F'.LaxMonoidal] → (f : F ⟶ F') → [CategoryTheory.NatTrans.IsMonoidal f] → F.mapMon ⟶ F'.mapMon
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingHom.surjective_codRestrict : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {σS : Type u_2}
  [inst_2 : SetLike σS S] [inst_3 : SubsemiringClass σS S] {f : R →+* S} {s : σS} {h : ∀ (x : R), f x ∈ s},
  Function.Surjective ⇑(f.codRestrict s h) ↔ f.rangeS = Subsemiring.ofClass s
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.NullMeasurableSet.mono_ac : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → ν.AbsolutelyContinuous μ → MeasureTheory.NullMeasurableSet s ν
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Cfg.inhabited : {K : Type u_1} → (Γ : K → Type u_2) → (Λ : Type u_3) → (σ : Type u_4) → [Inhabited σ] → Inhabited (Turing.TM2.Cfg Γ Λ σ)
-- Mathlib.RingTheory.RootsOfUnity.Complex
Complex.isPrimitiveRoot_exp : ∀ (n : ℕ), n ≠ 0 → IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
-- Init.Data.SInt.Lemmas
Int16.ofBitVec_sdiv : ∀ (a b : BitVec 16), Int16.ofBitVec (a.sdiv b) = Int16.ofBitVec a / Int16.ofBitVec b
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.toSubgroup_prod : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] {H : Type u_2} [inst_2 : Group H]
  [inst_3 : TopologicalSpace H] (U : OpenSubgroup G) (V : OpenSubgroup H), ↑(U.prod V) = (↑U).prod ↑V
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.le_extendScalars_iff : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F E : IntermediateField K L}
  (h : F ≤ E) (E' : IntermediateField (↥F) L),
  E' ≤ IntermediateField.extendScalars h ↔ IntermediateField.restrictScalars K E' ≤ E
-- Mathlib.Analysis.Normed.Group.Continuity
/-- Special case of the sandwich theorem: if the norm of `f` is bounded by a real function `a` which
tends to `0`, then `f` tends to `1`.  -/
squeeze_one_norm : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedGroup E] {f : α → E} {a : α → ℝ} {t₀ : Filter α},
  (∀ (n : α), ‖f n‖ ≤ a n) → Filter.Tendsto a t₀ (nhds 0) → Filter.Tendsto f t₀ (nhds 1)
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.truncFinset_coe_eq_self_iff : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {s : Finset (σ →₀ ℕ)} (p : MvPolynomial σ R),
  (MvPowerSeries.truncFinset R s) ↑p = p ↔ p.support ⊆ s
-- Lean.Meta.Tactic.Grind.Types
/-- Accumulated E-matching instance map for precise unused lemma tracking.
Only populated when `config.markInstances` is `true`.  -/
Lean.Meta.Grind.State.instanceMap : Lean.Meta.Grind.State → Std.HashMap Lean.Name Lean.Meta.Grind.EMatchTheorem
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsBasis'.contract_indep_iff : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α},
  M.IsBasis' I X → ((M.contract X).Indep J ↔ M.Indep (J ∪ I) ∧ Disjoint X J)
-- Mathlib.CategoryTheory.Products.Associator
CategoryTheory.prod.prodμ_unitIso_hom_app : ∀ (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] (A : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A] (X : (A × C) × D × E),
  (CategoryTheory.prod.prodμ C D E A).unitIso.hom.app X =
    CategoryTheory.Prod.mkHom
      (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1.1) (CategoryTheory.CategoryStruct.id X.1.2))
      (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.2.1) (CategoryTheory.CategoryStruct.id X.2.2))
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.instSMulInt : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} → {Y : Type u_2} → [inst_1 : AddGroup Y] → SMul ℤ (Function.locallyFinsuppWithin U Y)
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.OplaxTrans.Hom.of.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} {as as_1 : CategoryTheory.Lax.OplaxTrans.Modification η θ},
  { as := as } = { as := as_1 } → as = as_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.nonsingular_iff_of_Y_eq_negY : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F},
  P 2 ≠ 0 → P 1 = W.negY P → (W.Nonsingular P ↔ W.Equation P ∧ (MvPolynomial.eval P) W.polynomialX ≠ 0)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_alter_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α} [inst : Inhabited β] {f : Option β → Option β},
  Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl k =
    (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).get!
-- Mathlib.Algebra.Ring.Units
Units.divp_sub : ∀ {α : Type u} [inst : Ring α] (a b : α) (u : αˣ), a /ₚ u - b = (a - b * ↑u) /ₚ u
-- Mathlib.Data.Set.Image
Set.disjoint_image_left : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β}, Disjoint (f '' s) t ↔ Disjoint s (f ⁻¹' t)
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- The `n`-cliques in a graph as a set.  -/
SimpleGraph.cliqueSet : {α : Type u_1} → SimpleGraph α → ℕ → Set (Finset α)
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
/-- We verify that the biproduct we've just defined is isomorphic to the `ModuleCat R` structure
on the dependent function type.
 -/
ModuleCat.biproductIsoPi : {R : Type u} →
  [inst : Ring R] → {J : Type} → [inst_1 : Finite J] → (f : J → ModuleCat R) → ⨁ f ≅ ModuleCat.of R ((j : J) → ↑(f j))
-- Mathlib.Algebra.Group.Action.Pretransitive
/-- `M` acts pretransitively on `α` if for any `x y` there is `g` such that `g +ᵥ x = y`.
A transitive action should furthermore have `α` nonempty.  -/
AddAction.IsPretransitive : (M : Type u_5) → (α : Type u_6) → [VAdd M α] → Prop
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.prod_cons : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (i : ι) (m : M i) (w : Monoid.CoprodI.Word M)
  (h1 : m ≠ 1) (h2 : w.fstIdx ≠ some i), (Monoid.CoprodI.Word.cons m w h2 h1).prod = Monoid.CoprodI.of m * w.prod
-- Mathlib.Geometry.Manifold.Instances.Icc
instOneTangentSpaceRealModelWithCornersSelf : (x : ℝ) → One (TangentSpace (modelWithCornersSelf ℝ ℝ) x)
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitSphere.instGroup : {𝕜 : Type u_1} → [inst : NormedDivisionRing 𝕜] → Group ↑(Metric.sphere 0 1)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.tensorUnit_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C], CategoryTheory.MonObj.one = CategoryTheory.MonObj.one
-- Mathlib.Algebra.BigOperators.Finprod
finprod_pow : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M},
  Function.HasFiniteMulSupport f → ∀ (n : ℕ), (∏ᶠ (i : α), f i) ^ n = ∏ᶠ (i : α), f i ^ n
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_insertIfNew_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insertIfNew k v).size ≤ t.size + 1
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Option.isSome.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((val : α) → motive (some val)) → (Unit → motive none) → motive x
-- Mathlib.Data.Sum.Order
/-- `Equiv.sumAssoc` promoted to an order isomorphism.  -/
OrderIso.sumAssoc : (α : Type u_10) →
  (β : Type u_11) → (γ : Type u_12) → [inst : LE α] → [inst_1 : LE β] → [inst_2 : LE γ] → (α ⊕ β) ⊕ γ ≃o α ⊕ β ⊕ γ
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.one_def : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Zero M], 1 = AddMonoidAlgebra.single 0 1
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.TransversalPair.mk.inj : ∀ {G : Type u_1} {inst : Group G} {A B : Subgroup G} {set : ℤˣ → Set G}
  {compl : ∀ (u : ℤˣ), Subgroup.IsComplement (↑(HNNExtension.toSubgroup A B u)) (set u)} {set_1 : ℤˣ → Set G}
  {compl_1 : ∀ (u : ℤˣ), Subgroup.IsComplement (↑(HNNExtension.toSubgroup A B u)) (set_1 u)},
  { set := set, compl := compl } = { set := set_1, compl := compl_1 } → set = set_1
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.seq : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α β : Type u}
  {post : β → Pred} {epost : EPred} (x : m (α → β)) (y : m α),
  ⦃ Std.Internal.Do.wp x (fun f => Std.Internal.Do.wp y (fun a => post (f a)) epost) epost ⦄ x <*> y ⦃ post; epost ⦄