mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.instMonoFιTruncLE : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncLE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] (i' : ι'), CategoryTheory.Mono ((K.ιTruncLE e).f i')
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point.0.WeierstrassCurve.Jacobian.nonsingular_add_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Nonsingular P →
    W.Nonsingular Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          ¬(P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 ∧ P 1 * Q 2 ^ 3 = W.negY Q * P 2 ^ 3) →
            W.Nonsingular
              ![W.toAffine.addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2)
                  (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)),
                W.toAffine.addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3)
                  (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)),
                1]
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.Lan.CommuteWith.instHasLeftKanExtensionComp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c)
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g] {x : B} (h : c ⟶ x)
  [CategoryTheory.Bicategory.Lan.CommuteWith f g h],
  CategoryTheory.Bicategory.HasLeftKanExtension f (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.calc_deriv_dist : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]},
  ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 →
    ∀ {z z' z1 : ℤ_[p]},
      z' = z - z1 →
        ‖z1‖ = ‖(Polynomial.aeval z) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ →
          ∀ {n : ℕ},
            ih_gen✝ n z →
              ‖(Polynomial.aeval z') (Polynomial.derivative F) - (Polynomial.aeval z) (Polynomial.derivative F)‖ <
                ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.sym.debug : Lean.Option Bool
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.curryRight_apply : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G)
  (m : (i : Fin n) → Ei i.castSucc) (x : Ei (Fin.last n)), (f.curryRight m) x = f (Fin.snoc m x)
-- Init.Tactics
/-- `repeat' tac` recursively applies `tac` on all of the goals so long as it succeeds.
That is to say, if `tac` produces multiple subgoals, then `repeat' tac` is applied to each of them.

See also:
* `repeat tac` simply repeatedly applies `tac`.
* `repeat1' tac` is `repeat' tac` but requires that `tac` succeed for some goal at least once.
 -/
Lean.Parser.Tactic.repeat' : Lean.ParserDescr
-- Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
MvPowerSeries.mem_nonZeroDivisorsLeft_of_constantCoeff : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {φ : MvPowerSeries σ R},
  MvPowerSeries.constantCoeff φ ∈ nonZeroDivisorsLeft R → φ ∈ nonZeroDivisorsLeft (MvPowerSeries σ R)
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.unop_le_unop_iff : ∀ {M : Type u_2} [inst : AddZeroClass M] {S₁ S₂ : AddSubmonoid Mᵃᵒᵖ}, S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂
-- Mathlib.Data.ENNReal.Operations
ENNReal.image_coe_Ico : ∀ (x y : NNReal), ENNReal.ofNNReal '' Set.Ico x y = Set.Ico ↑x ↑y
-- Qq.Macro
Qq.Impl.quoteLevelList : List Lean.Level → Qq.Impl.QuoteM Lean.Expr
-- Lean.Elab.ConfigEval.Basic
/-- Evaluate `stx` using either `evalStx` or `evalExpr`.
 -/
Lean.Elab.ConfigEval.evalTermOrExprWithElab : {α : Type} → [Lean.Elab.ConfigEval.EvalTerm α] → [Lean.Elab.ConfigEval.EvalExpr α] → Lean.Term → Lean.Elab.TermElabM α
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- Converse to the mean value inequality: if `f` is `C`-lipschitz then
its derivative at `x₀` has norm bounded by `C`.
Version using `fderiv`.  -/
norm_fderiv_le_of_lipschitz : ∀ (𝕜 : 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 : NNReal}, LipschitzWith C f → ‖fderiv 𝕜 f x₀‖ ≤ ↑C
-- Mathlib.Data.List.MinMax
List.coe_maximum_of_length_pos : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α} (h : 0 < l.length), ↑(List.maximum_of_length_pos h) = l.maximum
-- Mathlib.Logic.Nonempty
exists_const_iff : ∀ {α : Sort u_3} {P : Prop}, (∃ x, P) ↔ Nonempty α ∧ P
-- Mathlib.LinearAlgebra.FreeModule.Int
Int.submodule_toAddSubgroup_index_ne_zero_iff : ∀ {ι : Type u_1} [Finite ι] {N : Submodule ℤ (ι → ℤ)}, N.toAddSubgroup.index ≠ 0 ↔ Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)
-- Mathlib.Data.Multiset.AddSub
Multiset.card_sub : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, t ≤ s → (s - t).card = s.card - t.card
-- Lean.Meta.Tactic.Grind.Arith.Linear.Reify
Lean.Meta.Grind.Arith.Linear.isHSMulIntInst : Lean.Meta.Grind.Arith.Linear.Struct → Lean.Expr → Bool
-- Mathlib.Analysis.Complex.Basic
Complex.mem_slitPlane_or_neg_mem_slitPlane : ∀ {z : ℂ}, z ≠ 0 → z ∈ Complex.slitPlane ∨ -z ∈ Complex.slitPlane
-- Mathlib.CategoryTheory.Category.Quiv
/-- The functor sending each quiver to its path category.  -/
CategoryTheory.Cat.free : CategoryTheory.Functor CategoryTheory.Quiv CategoryTheory.Cat
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
linearIndependent_algHom_toLinearMap' : ∀ (K : Type u_6) (M : Type u_7) (L : Type u_8) [inst : CommRing K] [IsDomain K] [inst_2 : Semiring M]
  [inst_3 : Algebra K M] [inst_4 : CommRing L] [IsDomain L] [inst_6 : Algebra K L] [Module.IsTorsionFree K L],
  LinearIndependent K AlgHom.toLinearMap
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_nonneg_of_nonpos_of_nonpos : ∀ {a b : ℤ}, a ≤ 0 → b ≤ 0 → 0 ≤ a.tdiv b
-- Mathlib.CategoryTheory.Comma.Basic
/-- The isomorphism between `map α β ⋙ snd L' R'` and `snd L R ⋙ F₂`,
where `β : R ⋙ F ⟶ F₂ ⋙ R'`.  -/
CategoryTheory.Comma.mapSnd : {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] →
            {B' : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} B'] →
                {A' : Type u₅} →
                  [inst_4 : CategoryTheory.Category.{v₅, u₅} A'] →
                    {T' : Type u₆} →
                      [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] →
                        {R : CategoryTheory.Functor B T} →
                          {L : CategoryTheory.Functor A T} →
                            {R' : CategoryTheory.Functor B' T'} →
                              {L' : CategoryTheory.Functor A' T'} →
                                {F₂ : CategoryTheory.Functor B B'} →
                                  {F₁ : CategoryTheory.Functor A A'} →
                                    {F : CategoryTheory.Functor T T'} →
                                      (β : F₁.comp L' ⟶ L.comp F) →
                                        (α : R.comp F ⟶ F₂.comp R') →
                                          (CategoryTheory.Comma.map β α).comp (CategoryTheory.Comma.snd L' R') ≅
                                            (CategoryTheory.Comma.snd L R).comp F₂
-- Mathlib.Algebra.Order.SuccPred
Order.le_of_lt_add_one : ∀ {α : Type u_1} {x y : α} [inst : LinearOrder α] [inst_1 : Add α] [inst_2 : One α] [SuccAddOrder α], x < y + 1 → x ≤ y
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_one : ∀ {α : Type u_2} [inst : One α], Finset.card 1 = 1
-- Init.Data.Vector.Lemmas
Vector.all_reverse : ∀ {α : Type u_1} {n : ℕ} {f : α → Bool} {xs : Vector α n}, xs.reverse.all f = xs.all f
-- Init.Data.UInt.Basic
/-- Non-strict inequality of 16-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the `≤` operator.
 -/
UInt16.le : UInt16 → UInt16 → Prop
-- Mathlib.Algebra.Algebra.Hom
/-- Defining the homomorphism in the category R-Alg, denoted `A →ₐ[R] B`.  -/
«term_→ₐ[_]_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.strictMap_singleton : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  (X : C) (F : CategoryTheory.Functor C D),
  (CategoryTheory.ObjectProperty.singleton X).strictMap F = CategoryTheory.ObjectProperty.singleton (F.obj X)
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
CategoryTheory.Limits.natTransIntoForgetCompFiberwiseColimit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H)
  [inst_2 :
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))]
  (X : CategoryTheory.Grothendieck F),
  (CategoryTheory.Limits.natTransIntoForgetCompFiberwiseColimit G).app X =
    CategoryTheory.Limits.colimit.ι ((CategoryTheory.Grothendieck.ι F X.base).comp G) X.fiber
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraQuaternion.j_quaternionBasis : ∀ {R : Type u_1} [inst : CommRing R] (c₁ c₂ : R),
  (CliffordAlgebraQuaternion.quaternionBasis c₁ c₂).j = (CliffordAlgebra.ι (CliffordAlgebraQuaternion.Q c₁ c₂)) (0, 1)
-- Init.Data.Int.Order
Int.ofNat_max_zero : ∀ (n : ℕ), max (↑n) 0 = ↑n
-- Qq.Macro
Qq.Impl.substLevel : Lean.Name → Lean.Level → Qq.Impl.UnquoteM Unit
-- Mathlib.Algebra.Category.Ring.Basic
/-- Ring equivalences are isomorphisms in category of commutative rings  -/
RingEquiv.toCommRingCatIso : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → R ≃+* S → (CommRingCat.of R ≅ CommRingCat.of S)
-- Mathlib.Algebra.Torsor.Defs
/-- An `AddTorsor G P` gives a structure to the nonempty type `P`,
acted on by an `AddGroup G` with a transitive and free action given
by the `+ᵥ` operation and a corresponding subtraction given by the
`-ᵥ` operation. In the case of a vector space, it is an affine
space.  -/
AddTorsor : (G : outParam (Type u_1)) → Type u_2 → [AddGroup G] → Type (max u_1 u_2)
-- Std.Data.TreeMap.Slice
Std.TreeMap.instSliceableRocSlice : {α : Type u} →
  {β : Type v} →
    (cmp : autoParam (α → α → Ordering) Std.TreeMap.instSliceableRocSlice._auto_1) →
      Std.Roc.Sliceable (Std.TreeMap α β cmp) α (Std.DTreeMap.Internal.Const.RocSlice α β)
-- Mathlib.Topology.Algebra.Ring.Basic
Subring.continuousSMul : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Ring R] (s : Subring R) (X : Type u_2)
  [inst_2 : TopologicalSpace X] [inst_3 : MulAction R X] [ContinuousSMul R X], ContinuousSMul (↥s) X
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.induction_on₂ : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  {α' : Type u_5} {β' : Type u_6} [inst_2 : MeasurableSpace α'] [inst_3 : TopologicalSpace β']
  {μ' : MeasureTheory.Measure α'} (f : α →ₘ[μ] β) (f' : α' →ₘ[μ'] β') {p : (α →ₘ[μ] β) → (α' →ₘ[μ'] β') → Prop},
  (∀ (f : α → β) (hf : MeasureTheory.AEStronglyMeasurable f μ) (f' : α' → β')
      (hf' : MeasureTheory.AEStronglyMeasurable f' μ'),
      p (MeasureTheory.AEEqFun.mk f hf) (MeasureTheory.AEEqFun.mk f' hf')) →
    p f f'
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.mk.injEq : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] {L : Type u_3}
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] {x : L →ₗ⁅R⁆ LieDerivation R K K} (left : K) (right : L) (left_1 : K)
  (right_1 : L),
  ({ left := left, right := right } = { left := left_1, right := right_1 }) = (left = left_1 ∧ right = right_1)
-- Mathlib.GroupTheory.Coprod.Basic
MulEquiv.coprodAssoc_apply_inl_inr : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : Monoid P] (x : N),
  (MulEquiv.coprodAssoc M N P) (Monoid.Coprod.inl (Monoid.Coprod.inr x)) = Monoid.Coprod.inr (Monoid.Coprod.inl x)
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.upperCentralSeries.eq_ge_of_eq_succ`. -/
upperCentralSeries.eq_ge_of_eq_succ : ∀ {G : Type u_1} [inst : Group G] {a b : ℕ},
  a ≤ b →
    Subgroup.upperCentralSeries G a = Subgroup.upperCentralSeries G (a + 1) →
      Subgroup.upperCentralSeries G a = Subgroup.upperCentralSeries G b
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.casesOn.eq_1 : ∀ {α : Type u_1} {motive : FreeAddMonoid α → Sort u_6} (xs : FreeAddMonoid α) (one : motive 0)
  (of_mul : (x : α) → (xs : FreeAddMonoid α) → motive (FreeAddMonoid.of x + xs)),
  FreeAddMonoid.casesOn xs one of_mul = List.casesOn xs one of_mul
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.concatRec.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} {motive : (u v : V) → G.Walk u v → Sort u_1}
  (Hnil : {u : V} → motive u u SimpleGraph.Walk.nil)
  (Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)) {u v : V}
  (p : G.Walk u v), SimpleGraph.Walk.concatRec Hnil Hconcat p = ⋯ ▸ SimpleGraph.Walk.concatRecAux Hnil Hconcat p.reverse
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
/-- `Multiseries`-part of `MultiseriesExpansion.monomial`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomial : (basis_hd : ℝ → ℝ) →
  (basis_tl : Tactic.ComputeAsymptotics.Basis) →
    ℕ → Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
/-- The notation `\textf` for `WeierstrassCurve.Jacobian.baseChange W S`.  -/
WeierstrassCurve.Jacobian.«term_⁄_» : Lean.TrailingParserDescr
-- Init.System.FilePath
System.instDecidableEqFilePath.decEq : (x x_1 : System.FilePath) → Decidable (x = x_1)
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- **Alias** of `MonoidHom.pi_apply`. -/
Pi.monoidHom_apply : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → MulOneClass (f i)] {γ : Type w} [inst_1 : MulOneClass γ]
  (g : (i : I) → γ →* f i) (x : γ) (i : I), (MonoidHom.pi g) x i = (g i) x
-- Mathlib.Topology.Order.OrderClosed
isClosed_le : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α]
  [inst_2 : TopologicalSpace β] {f g : β → α}, Continuous f → Continuous g → IsClosed {b | f b ≤ g b}
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePushout.arrow_ι_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
  (arrows : (j : J) → B ⟶ objs j) [inst_1 : CategoryTheory.Limits.HasWidePushout B objs arrows] (j : J) {Z : C}
  (h : CategoryTheory.Limits.widePushout B objs arrows ⟶ Z),
  CategoryTheory.CategoryStruct.comp (arrows j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.ι arrows j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.head arrows) h
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.inv_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Inv Y] (f : LocallyConstant X Y) (x : X),
  f⁻¹ x = (f x)⁻¹
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.isIso_ι_initial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  [inst_2 : CategoryTheory.Limits.HasInitial J] (F : CategoryTheory.Functor J C)
  [inst_3 : ∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)],
  CategoryTheory.IsIso (CategoryTheory.Limits.colimit.ι F (⊥_ J))
-- Batteries.Tactic.Alias
/-- Reverse direction of an iff alias  -/
Batteries.Tactic.Alias.AliasInfo.reverse : Lean.Name → Batteries.Tactic.Alias.AliasInfo
-- Mathlib.CategoryTheory.Sites.SheafOfTypes
CategoryTheory.Presieve.yonedaFamilyOfElements_fromCocone.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (R : CategoryTheory.Presieve X)
  (s : CategoryTheory.Limits.Cocone R.diagram) ⦃Y : C⦄ (f f_1 : Y ⟶ X) (e_f : f = f_1) (a : R f),
  R.yonedaFamilyOfElements_fromCocone s f a = R.yonedaFamilyOfElements_fromCocone s f_1 ⋯
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
tendstoLocallyUniformly_iff_forall_isCompact : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {p : Filter ι} [LocallyCompactSpace α],
  TendstoLocallyUniformly F f p ↔ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn F f p K
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.destruct.eq_1 : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl),
  ms.destruct =
    Option.map
      (fun x =>
        match x with
        | ((exp, coef), tl) => (exp, coef, tl))
      (Stream'.Seq.destruct ms)
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.instNoNatZeroDivisorsQOfAddRightCancel : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] [Lean.Grind.AddRightCancel α] [Lean.Grind.NoNatZeroDivisors α],
  Lean.Grind.NoNatZeroDivisors (Lean.Grind.IntModule.OfNatModule.Q α)
-- Mathlib.Algebra.Ring.Subsemiring.Defs
natCast_mem : ∀ {S : Type u_1} {R : Type u_2} [inst : AddMonoidWithOne R] [inst_1 : SetLike S R] (s : S)
  [AddSubmonoidWithOneClass S R] (n : ℕ), ↑n ∈ s
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the elements of the given closed range as an array in ascending order.
 -/
Std.Rcc.toArray : {α : Type u} →
  [inst : LE α] →
    [DecidableLE α] →
      [inst_2 : Std.PRange.UpwardEnumerable α] →
        [Std.PRange.LawfulUpwardEnumerable α] → [Std.Rxc.IsAlwaysFinite α] → Std.Rcc α → Array α
-- Mathlib.Tactic.Translate.Core
/-- The arguments that should be reordered when translating, using cycle notation.  -/
Mathlib.Tactic.Translate.Config.reorder? : Mathlib.Tactic.Translate.Config → Option Mathlib.Tactic.Translate.ArgReorder
-- Mathlib.Data.Set.Image
Set.preimage_sdiff : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s t : Set β), f ⁻¹' (s \ t) = f ⁻¹' s \ f ⁻¹' t
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.mul_one : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} (X : C)
  [self : CategoryTheory.MonObj X],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.MonObj.one)
      CategoryTheory.MonObj.mul =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
-- Mathlib.Algebra.Order.GroupWithZero.Defs
lt_of_mul_lt_mul_right : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c : α} [MulPosReflectLT α],
  b * a < c * a → 0 ≤ a → b < c
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
IsAddUnit.finset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] {a : α}, IsAddUnit a → IsAddUnit {a}
-- Mathlib.Condensed.Light.Explicit
/-- A light condensed object preserves finite products.  -/
LightCondensed.instPreservesFiniteProductsOppositeLightProfiniteObjFunctorIsSheafCoherentTopology : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] (X : LightCondensed A),
  CategoryTheory.Limits.PreservesFiniteProducts X.obj
-- Mathlib.Algebra.Order.SuccPred
Order.add_one_le_of_lt : ∀ {α : Type u_1} {x y : α} [inst : Preorder α] [inst_1 : Add α] [inst_2 : One α] [SuccAddOrder α], x < y → x + 1 ≤ y
-- Lean.MetavarContext
Lean.MetavarContext.mk.sizeOf_spec : ∀ (depth levelAssignDepth lmvarCounter mvarCounter : ℕ)
  (lDecls : Lean.PersistentHashMap Lean.LMVarId Lean.LevelMetavarDecl)
  (decls : Lean.PersistentHashMap Lean.MVarId Lean.MetavarDecl)
  (userNames : Lean.PersistentHashMap Lean.Name Lean.MVarId)
  (lAssignment : Lean.PersistentHashMap Lean.LMVarId Lean.Level)
  (eAssignment : Lean.PersistentHashMap Lean.MVarId Lean.Expr)
  (dAssignment : Lean.PersistentHashMap Lean.MVarId Lean.DelayedMetavarAssignment),
  sizeOf
      { depth := depth, levelAssignDepth := levelAssignDepth, lmvarCounter := lmvarCounter, mvarCounter := mvarCounter,
        lDecls := lDecls, decls := decls, userNames := userNames, lAssignment := lAssignment,
        eAssignment := eAssignment, dAssignment := dAssignment } =
    1 + sizeOf depth + sizeOf levelAssignDepth + sizeOf lmvarCounter + sizeOf mvarCounter + sizeOf lDecls +
              sizeOf decls +
            sizeOf userNames +
          sizeOf lAssignment +
        sizeOf eAssignment +
      sizeOf dAssignment
-- Init.System.IOError
IO.Error.mkAlreadyExists : UInt32 → String → IO.Error
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
_private.Mathlib.GroupTheory.SpecificGroups.Quaternion.0.QuaternionGroup.mul.eq_3 : ∀ {n : ℕ} (a a_1 : ZMod (2 * n)),
  QuaternionGroup.mul✝ (QuaternionGroup.xa a) (QuaternionGroup.a a_1) = QuaternionGroup.xa (a + a_1)
-- Mathlib.Combinatorics.Graph.Basic
Graph.copy_isLink : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) {vertexSet : Set α} {edgeSet : Set β} {IsLink : β → α → α → Prop}
  (hvertexSet : G.vertexSet = vertexSet) (hedgeSet : G.edgeSet = edgeSet)
  (hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y) (a : β) (a_1 a_2 : α),
  (G.copy hvertexSet hedgeSet hIsLink).IsLink a a_1 a_2 = IsLink a a_1 a_2
-- Mathlib.RingTheory.Localization.Away.Basic
selfZPow_of_nonpos : ∀ {R : Type u_1} [inst : CommSemiring R] (x : R) (B : Type u_2) [inst_1 : CommSemiring B] [inst_2 : Algebra R B]
  [inst_3 : IsLocalization.Away x B] {n : ℤ}, n ≤ 0 → selfZPow x B n = IsLocalization.mk' B 1 (Submonoid.pow x n.natAbs)
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.toFun : {α : Type u} →
  {β : Type v} →
    [inst : Std.PRange.UpwardEnumerable α] →
      [inst_1 : Std.PRange.UpwardEnumerable β] → Std.PRange.UpwardEnumerable.Map α β → α → β
-- Init.Data.FloatArray.Basic
FloatArray.uget : (a : FloatArray) → (i : USize) → i.toNat < a.size → Float
-- Lean.PrettyPrinter.Delaborator.Builtins
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.evalSyntaxConstant : Lean.Environment → Lean.Options → Lean.Name → ExceptT String Id Lean.Syntax
-- Mathlib.Algebra.Star.Subalgebra
Subalgebra.mem_star_iff : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (S : Subalgebra R A) (x : A),
  x ∈ star S ↔ star x ∈ S
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.nthRoots.congr_simp : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (n n_1 : ℕ),
  n = n_1 → ∀ (a a_1 : R), a = a_1 → Polynomial.nthRoots n a = Polynomial.nthRoots n_1 a_1
-- Mathlib.Order.Category.Frm
Frm.str : (self : Frm) → Order.Frame ↑self
-- Mathlib.Analysis.Calculus.ContDiff.Comp
Differentiable.fderiv_two : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F → G} {g : E → F},
  ContDiff 𝕜 2 (Function.uncurry f) → ContDiff 𝕜 1 g → Differentiable 𝕜 fun x => fderiv 𝕜 (f x) (g x)
-- Mathlib.Order.Filter.Defs
/-- The product of an indexed family of filters.  -/
Filter.pi : {ι : Type u_3} → {α : ι → Type u_4} → ((i : ι) → Filter (α i)) → Filter ((i : ι) → α i)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.instEpiModuleCatH1π : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.Epi (groupHomology.H1π A)