mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Http.Internal.ChunkedBuffer
Std.Http.Internal.ChunkedBuffer.mk.inj : ∀ {data : Array ByteArray} {size : ℕ} {data_1 : Array ByteArray} {size_1 : ℕ},
  { data := data, size := size } = { data := data_1, size := size_1 } → data = data_1 ∧ size = size_1
-- Mathlib.RingTheory.WittVector.Isocrystal
WittVector.inv_pair₂ : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (k : Type u_1) [inst_1 : CommRing k] [inst_2 : CharP k p]
  [inst_3 : PerfectRing k p],
  RingHomInvPair ↑(WittVector.FractionRing.frobenius p k).symm ↑(WittVector.FractionRing.frobenius p k)
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
/-- The limit of `(1 + g x) ^ x` as `(x : ℝ) → ∞` is `exp t`,
where `t : ℝ` is the limit of `x * g x`.  -/
Real.tendsto_one_add_rpow_exp_of_tendsto : ∀ {g : ℝ → ℝ} {t : ℝ},
  Filter.Tendsto (fun x => x * g x) Filter.atTop (nhds t) →
    Filter.Tendsto (fun x => (1 + g x) ^ x) Filter.atTop (nhds (Real.exp t))
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapMonCompIso_hom_app_hom : ∀ {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] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [inst_6 : F.LaxMonoidal] [inst_7 : G.LaxMonoidal]
  (X : CategoryTheory.Mon C),
  (CategoryTheory.Functor.mapMonCompIso.hom.app X).hom = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.X))
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
spectralNorm.spectralMulAlgNorm_eq_of_mem_roots : ∀ (K : Type u) [inst : NontriviallyNormedField K] (L : Type v) [inst_1 : Field L] [inst_2 : Algebra K L]
  [hu : IsUltrametricDist K] [inst_3 : CompleteSpace K] (x : L) {E : Type u_2} [inst_4 : Field E] [inst_5 : Algebra K E]
  [inst_6 : Algebra L E] [IsScalarTower K L E] [inst_8 : Algebra.IsAlgebraic K E] {a : E},
  a ∈ ((Polynomial.mapAlg K E) (minpoly K x)).roots →
    (spectralMulAlgNorm K E) a = (spectralMulAlgNorm K E) ((algebraMap L E) x)
-- Mathlib.Data.Ordmap.Ordnode
/-- Auxiliary definition for `ofAscList`.

**Note:** This function is defined by well-founded recursion, so it will probably not compute
in the kernel, meaning that you probably can't prove things like
`ofAscList [1, 2, 3] = {1, 2, 3}` by `rfl`.
This implementation is optimized for VM evaluation.  -/
Ordnode.ofAscListAux₁ : {α : Type u_1} → (l : List α) → ℕ → Ordnode α × { l' // l'.length ≤ l.length }
-- Mathlib.Data.Finsupp.AList
/-- Produce an association list for the finsupp over its support using choice.  -/
Finsupp.toAList : {α : Type u_1} → {M : Type u_2} → [inst : Zero M] → (α →₀ M) → AList fun _x => M
-- Mathlib.Algebra.Order.Antidiag.Prod
/-- In a canonically ordered multiplicative monoid, the mulAntidiagonal can be constructed by
filtering.

Note that this is not an instance, as for sometimes a more efficient algorithm is available.  -/
Finset.HasMulAntidiagonal.mulAntidiagonalOfLocallyFinite : {A : Type u_2} →
  [inst : CommMonoid A] →
    [inst_1 : PartialOrder A] →
      [CanonicallyOrderedMul A] → [LocallyFiniteOrderBot A] → [DecidableEq A] → Finset.HasMulAntidiagonal A
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constMaxEntry!_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited (α × β)],
  t₁.WF →
    t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Internal.Impl.Const.maxEntry! t₁ = Std.DTreeMap.Internal.Impl.Const.maxEntry! t₂
-- Mathlib.Algebra.Tropical.Lattice
instInfSetTropical : {R : Type u_1} → [InfSet R] → InfSet (Tropical R)
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.List.toAssocList.match_1.eq_2 : ∀ {α : Type u_2} {β : Type u_1} (motive : List (α × β) → Sort u_3) (a : α) (b : β) (es : List (α × β))
  (h_1 : Unit → motive []) (h_2 : (a : α) → (b : β) → (es : List (α × β)) → motive ((a, b) :: es)),
  (match (a, b) :: es with
    | [] => h_1 ()
    | (a, b) :: es => h_2 a b es) =
    h_2 a b es
-- Mathlib.Data.Nat.Count
/-- `count p n` can be expressed as the cardinality of `{k // k < n ∧ p k}`.  -/
Nat.count_eq_card_fintype : ∀ (p : ℕ → Prop) [inst : DecidablePred p] (n : ℕ), Nat.count p n = Fintype.card { k // k < n ∧ p k }
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorInfo.recursorName : Lean.Meta.RecursorInfo → Lean.Name
-- Mathlib.Order.SupClosed
supClosure_singleton : ∀ {α : Type u_3} [inst : SemilatticeSup α] {a : α}, supClosure {a} = {a}
-- Mathlib.LinearAlgebra.Matrix.WithConv
instStarAddMonoidWithConvMatrix : {m : Type u_1} →
  {n : Type u_2} → {α : Type u_3} → [inst : AddMonoid α] → [StarAddMonoid α] → StarAddMonoid (WithConv (Matrix m n α))
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.eraseMin.match_1.eq_3 : ∀ {α : Type u_1} (motive : Ordnode α → Sort u_2) (size sz : ℕ) (l' : Ordnode α) (y : α) (r' : Ordnode α) (x : α)
  (r : Ordnode α) (h_1 : Unit → motive Ordnode.nil)
  (h_2 : (size : ℕ) → (x : α) → (r : Ordnode α) → motive (Ordnode.node size Ordnode.nil x r))
  (h_3 :
    (size sz : ℕ) →
      (l' : Ordnode α) →
        (y : α) →
          (r' : Ordnode α) → (x : α) → (r : Ordnode α) → motive (Ordnode.node size (Ordnode.node sz l' y r') x r)),
  (match Ordnode.node size (Ordnode.node sz l' y r') x r with
    | Ordnode.nil => h_1 ()
    | Ordnode.node size Ordnode.nil x r => h_2 size x r
    | Ordnode.node size (Ordnode.node sz l' y r') x r => h_3 size sz l' y r' x r) =
    h_3 size sz l' y r' x r
-- Mathlib.NumberTheory.PrimeCounting
Nat.primeCounting_eq_primeCounting'_succ : ∀ (n : ℕ), n.primeCounting = (n + 1).primeCounting'
-- Batteries.Data.ByteArray
ByteArray.get_set_ne : ∀ {j : ℕ} (a : ByteArray) (i : Fin a.size) (v : UInt8) (hj : j < a.size), ↑i ≠ j → (a.set (↑i) v ⋯)[j] = a[j]
-- Mathlib.Analysis.SpecialFunctions.Arcosh
Real.contDiffAt_arcosh : ∀ {n : WithTop ℕ∞} {x : ℝ}, x ∈ Set.Ioi 1 → ContDiffAt ℝ n Real.arcosh x
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_inter_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, k ∉ t₁ → (t₁ ∩ t₂).getD k fallback = fallback
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
/-- Return `(f, g)` if `e` is definitionally equal to `f ≫ g`.  -/
Mathlib.Tactic.Bicategory.comp? : Lean.Expr →
  Mathlib.Tactic.Bicategory.BicategoryM
    (Option (Mathlib.Tactic.BicategoryLike.Mor₁ × Mathlib.Tactic.BicategoryLike.Mor₁))
-- Mathlib.CategoryTheory.Comma.CardinalArrow
CategoryTheory.hasCardinalLT_arrow_shrink_iff : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : Small.{w', u} C] (κ : Cardinal.{w}),
  HasCardinalLT (CategoryTheory.Arrow (Shrink.{w', u} C)) κ ↔ HasCardinalLT (CategoryTheory.Arrow C) κ
-- Mathlib.Tactic.ComputeDegree
/-- `compute_degree` is a tactic to solve goals of the form
*  `natDegree f = d`,
*  `degree f = d`,
*  `natDegree f ≤ d` (or `<`),
*  `degree f ≤ d` (or `<`),
*  `coeff f d = r`, if `d` is the degree of `f`.

The tactic may leave goals of the form `d' = d`, `d' ≤ d`, `d' < d`, or `r ≠ 0`, where `d'` in `ℕ`
or `WithBot ℕ` is the tactic's guess of the degree, and `r` is the coefficient's guess of the
leading coefficient of `f`.

`compute_degree` applies `norm_num` to the left-hand side of all side goals, trying to close them.

The variant `compute_degree!` first applies `compute_degree`.
Then it uses `norm_num` on all the remaining goals and tries `assumption`.
 -/
Mathlib.Tactic.ComputeDegree.tacticCompute_degree! : Lean.ParserDescr
-- Mathlib.Algebra.Notation.Pi.Basic
/-- On non-dependent functions, `Pi.mulSingle` is symmetric in the two indices.  -/
Pi.mulSingle_comm : ∀ {ι : Type u_1} [inst : DecidableEq ι] {M : Type u_9} [inst_1 : One M] (i : ι) (x : M) (j : ι),
  Pi.mulSingle i x j = Pi.mulSingle j x i
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The natural inclusion `B₂(G, A) →ₗ[k] Z₂(G, A)`.  -/
groupHomology.boundariesToCycles₂ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → ↥(groupHomology.boundaries₂ A) →ₗ[k] ↥(groupHomology.cycles₂ A)
-- Init.Data.Array.Lemmas
Array.flatMap_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs : Array α} {f : α → Array β} {g : β → Array γ},
  Array.flatMap g (Array.flatMap f xs) = Array.flatMap (fun x => Array.flatMap g (f x)) xs
-- Mathlib.Data.Fin.VecNotation
Matrix.cons_val_three : ∀ {α : Type u} {m : ℕ} (x : α) (u : Fin m.succ.succ.succ → α),
  Matrix.vecCons x u 3 = Matrix.vecHead (Matrix.vecTail (Matrix.vecTail u))
-- Mathlib.Analysis.Calculus.Deriv.Inverse
/-- If `f (g y) = y` for `y` in some neighborhood of `a`, `g` is continuous at `a`, and `f` has an
invertible derivative `f'` at `g a` in the strict sense, then `g` has the derivative `f'⁻¹` at `a`
in the strict sense.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an
inverse function.  -/
HasStrictDerivAt.of_local_left_inverse : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜} {f' a : 𝕜},
  ContinuousAt g a →
    HasStrictDerivAt f f' (g a) → f' ≠ 0 → (∀ᶠ (y : 𝕜) in nhds a, f (g y) = y) → HasStrictDerivAt g f'⁻¹ a
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprodXIso_hom_snd_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K L : HomologicalComplex C c)
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι) {Z : C} (h : L.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.biprodXIso L i).hom
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.snd.f i) h
-- Mathlib.Tactic.NormNum.Result
/-- A shortcut (non)instance for `Nat.AtLeastTwo (n + 2)` to shrink generated proofs.  -/
Mathlib.Meta.NormNum.instAtLeastTwo : ∀ (n : ℕ), (n + 2).AtLeastTwo
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
Mathlib.Tactic.Linarith.SimplexAlgorithm.SparseMatrix.mk : {n m : ℕ} → Array (Std.HashMap ℕ ℚ) → Mathlib.Tactic.Linarith.SimplexAlgorithm.SparseMatrix n m
-- Mathlib.Topology.Compactness.Compact
/-- The `CompactSpace` version of **Alexander's subbasis theorem**. If `X` is a topological space with a
subbasis `S`, then `X` is compact if for any open cover of `X` all of whose elements belong to `S`,
there is a finite subcover.
 -/
compactSpace_generateFrom : ∀ {X : Type u} [T : TopologicalSpace X] {S : Set (Set X)},
  T = TopologicalSpace.generateFrom S →
    (∀ P ⊆ S, ⋃₀ P = Set.univ → ∃ Q ⊆ P, Q.Finite ∧ ⋃₀ Q = Set.univ) → CompactSpace X
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Simprocs : Type
-- Mathlib.Topology.Covering.Basic
IsFiberBundle.isCoveringMap : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {F : Type u_3}
  [inst_2 : TopologicalSpace F] [DiscreteTopology F], (∀ (x : X), ∃ e, x ∈ e.baseSet) → IsCoveringMap f
-- Mathlib.Analysis.Complex.Exponential
Real.exp_sub : ∀ (x y : ℝ), Real.exp (x - y) = Real.exp x / Real.exp y
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.instNormal : ∀ {G : Type u} [inst : Group G] [inst_1 : TopologicalSpace G] (H : OpenNormalSubgroup G), (↑H.toOpenSubgroup).Normal
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.comp_apex : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C}
  [inst_1 : Wₗ.HasPullbacksAgainst Wᵣ] [inst_2 : Wₗ.IsStableUnderBaseChangeAgainst Wᵣ]
  [inst_3 : Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [inst_4 : Wₗ.IsStableUnderComposition]
  [inst_5 : Wᵣ.IsStableUnderComposition] {c c' c'' : C} (S₁ : CategoryTheory.Span Wₗ Wᵣ c c')
  (S₂ : CategoryTheory.Span Wₗ Wᵣ c' c''), (S₁.comp S₂).apex = CategoryTheory.Limits.pullback S₁.r S₂.l
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.add_lt_right_iff : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.AddCommMonoid M] [Lean.Grind.OrderedAdd M]
  [inst_4 : LT M] [Std.LawfulOrderLT M] {a b : M} (c : M), a < b ↔ c + a < c + b
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.Subtype.instHImp : {α : Type u_1} → [inst : MeasurableSpace α] → HImp (Subtype MeasurableSet)
-- Init.Data.SInt.Lemmas
ISize.toInt8_ofBitVec : ∀ (b : BitVec System.Platform.numBits), (ISize.ofBitVec b).toInt8 = Int8.ofBitVec (BitVec.signExtend 8 b)
-- Mathlib.Algebra.Ring.InjSurj
/-- Pullback a `NonAssocRing` instance along an injective function.  -/
Function.Injective.nonAssocRing : {R : Type u_1} →
  {S : Type u_2} →
    (f : S → R) →
      Function.Injective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : One S] →
                [inst_4 : Neg S] →
                  [inst_5 : Sub S] →
                    [inst_6 : SMul ℕ S] →
                      [inst_7 : SMul ℤ S] →
                        [inst_8 : NatCast S] →
                          [inst_9 : IntCast S] →
                            [inst_10 : NonAssocRing R] →
                              f 0 = 0 →
                                f 1 = 1 →
                                  (∀ (x y : S), f (x + y) = f x + f y) →
                                    (∀ (x y : S), f (x * y) = f x * f y) →
                                      (∀ (x : S), f (-x) = -f x) →
                                        (∀ (x y : S), f (x - y) = f x - f y) →
                                          (∀ (n : ℕ) (x : S), f (n • x) = n • f x) →
                                            (∀ (n : ℤ) (x : S), f (n • x) = n • f x) →
                                              (∀ (n : ℕ), f ↑n = ↑n) → (∀ (n : ℤ), f ↑n = ↑n) → NonAssocRing S
-- Mathlib.Algebra.Group.Support
Function.support_add_neg : ∀ {α : Type u_1} {G : Type u_3} [inst : SubtractionMonoid G] (f g : α → G),
  (Function.support fun x => f x + -g x) ⊆ Function.support f ∪ Function.support g
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
/-- Updates the old assignment of `l` to reflect the fact that `(l, true)` is no longer part of the
formula.
 -/
Std.Tactic.BVDecide.LRAT.Internal.Assignment.removePosAssignment : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Std.Tactic.BVDecide.LRAT.Internal.Assignment
-- Batteries.Data.Char.AsciiCasing
Char.toUpper_toLower_eq_toUpper : ∀ (c : Char), c.toLower.toUpper = c.toUpper
-- Mathlib.Algebra.Module.Basic
/-- If `E` is a vector space over two division rings `R` and `S`, then scalar multiplications
agree on inverses of integer numbers in `R` and `S`.  -/
inv_intCast_smul_eq : ∀ {E : Type u_5} (R : Type u_6) (S : Type u_7) [inst : AddCommGroup E] [inst_1 : DivisionRing R]
  [inst_2 : DivisionRing S] [inst_3 : Module R E] [inst_4 : Module S E] (n : ℤ) (x : E), (↑n)⁻¹ • x = (↑n)⁻¹ • x
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.SameCycle.eq_1 : ∀ {α : Type u_2} (f : Equiv.Perm α) (x y : α), f.SameCycle x y = ∃ i, (f ^ i) x = y
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.Hom.ext : ∀ {M N : SemiNormedGrp} {x y : M.Hom N}, x.hom' = y.hom' → x = y
-- Init.Classical
Classical.instNonemptyDecidable : ∀ (a : Prop), Nonempty (Decidable a)
-- Mathlib.Topology.Metrizable.Basic
/-- Given an embedding of a topological space into a metrizable space, the source space is also
metrizable.  -/
Topology.IsEmbedding.metrizableSpace : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [TopologicalSpace.MetrizableSpace Y] {f : X → Y}, Topology.IsEmbedding f → TopologicalSpace.MetrizableSpace X
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
inl_coprodIsoPushout_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct X Y],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (coprodIsoPushout X Y).hom =
    CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)
-- Mathlib.NumberTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.inertiaDeg'_comap_eq`. -/
Ideal.inertiaDeg_comap_eq : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  {S₁ : Type u_1} [inst_3 : CommRing S₁] [inst_4 : Algebra R S₁] (e : S ≃ₐ[R] S₁) (P : Ideal S₁),
  p.inertiaDeg' (Ideal.comap e P) = p.inertiaDeg' P
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.eq_top_iff : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] {S : NonUnitalStarSubalgebra R A}, S = ⊤ ↔ ∀ (x : A), x ∈ S
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.comp.inj : ∀ {C : Type u} {X Y Z : CategoryTheory.FreeMonoidalCategory C} {f : X.Hom Y} {g : Y.Hom Z}
  {Y_1 : CategoryTheory.FreeMonoidalCategory C} {f_1 : X.Hom Y_1} {g_1 : Y_1.Hom Z},
  f.comp g = f_1.comp g_1 → Y = Y_1 ∧ f ≍ f_1 ∧ g ≍ g_1
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min?_bind_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → t.min?.bind t.get? = t.min?
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.collectArg : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Arg pu → Lean.FVarIdHashSet → Lean.FVarIdHashSet
-- Mathlib.Analysis.LocallyConvex.SeparatingDual
separatingDual_def : ∀ (R : Type u_1) (V : Type u_2) [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace V]
  [inst_3 : TopologicalSpace R] [inst_4 : Module R V], SeparatingDual R V ↔ ∀ (x : V), x ≠ 0 → ∃ f, f x ≠ 0
-- Aesop.Frontend.Tactic
Aesop.Frontend.TacticConfig.additionalRules : Aesop.Frontend.TacticConfig → Array Aesop.Frontend.RuleExpr
-- Lean.Server.FileWorker.Utils
/-- Appends new non-sticky diagnostics.  -/
Lean.Server.FileWorker.EditableDocumentCore.appendDiagnostics : Lean.Server.FileWorker.EditableDocumentCore → Array Lean.Widget.InteractiveDiagnostic → BaseIO Unit
-- Mathlib.CategoryTheory.Sites.Precoverage
/-- A precoverage has isomorphisms if singleton presieves by isomorphisms are covering.  -/
CategoryTheory.Precoverage.HasIsos : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Precoverage C → Prop
-- Mathlib.Logic.Equiv.Basic
Equiv.coe_piCongr' : ∀ {α : Sort u_1} {β : Sort u_4} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : (b : β) → W (h₁.symm b) ≃ Z b),
  ⇑(h₁.piCongr' h₂) = fun f b => (h₂ b) (f (h₁.symm b))
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.volume_pi_pi : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasureTheory.MeasureSpace (α i)]
  [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] (s : (i : ι) → Set (α i)),
  MeasureTheory.volume (Set.univ.pi s) = ∏ i, MeasureTheory.volume (s i)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.isIso_colimMap : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasColimit G] (α : G ⟶ F) [CategoryTheory.IsIso α],
  CategoryTheory.IsIso (CategoryTheory.Limits.colimMap α)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.preΨ'_ne_zero : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [Nontrivial R] {n : ℕ}, ↑n ≠ 0 → W.preΨ' n ≠ 0
-- Init.Data.List.Lemmas
List.all_bne : ∀ {α : Type u_1} {a : α} [inst : BEq α] {l : List α}, (l.all fun x => a != x) = !l.contains a
-- Init.Data.Int.Order
Int.sub_lt_sub : ∀ {a b c d : ℤ}, a < b → c < d → a - d < b - c
-- Lean.Parser.Do
Lean.Parser.Term.doMatchExpr.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.HasSubst.substInv : ∀ {R : Type u_2} [inst : CommRing R] (P : PowerSeries R) [inst_1 : Invertible ((PowerSeries.coeff 1) P)],
  PowerSeries.HasSubst P.substInv
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min!_eq_default : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = true → t.min! = default
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Preconnected.set_univ_walk_nonempty : ∀ {V : Type u} {G : SimpleGraph V}, G.Preconnected → ∀ (u v : V), Set.univ.Nonempty
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.hasProjectiveDimensionLT_zero_iff_isZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C),
  CategoryTheory.HasProjectiveDimensionLT X 0 ↔ CategoryTheory.Limits.IsZero X
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_inv_hom_id_assoc : ∀ {C : Type u_1} {ι' : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁)
  (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ)
  (h : CategoryTheory.Limits.IsZero ((X'.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hi₃₄))))
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_inv_hom_id._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_inv_hom_id._auto_3) {Z : C}
  (h_1 :
    X'.E (CategoryTheory.homOfLE hi₀₁) (CategoryTheory.homOfLE hi₁₂) (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X'.isoMapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).inv
      (CategoryTheory.CategoryStruct.comp (X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂) h_1) =
    h_1
-- Init.Data.Iterators.Producers.Monadic.List
Std.Iterators.Types.ListIterator.instIterator : {m : Type w → Type w'} → {α : Type w} → [Pure m] → Std.Iterator (Std.Iterators.Types.ListIterator α) m α
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.right_unitality_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (n : M)
  (X : C) [inst_3 : F.Monoidal],
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.ε F).app ((F.obj n).obj X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Functor.LaxMonoidal.μ F n (CategoryTheory.MonoidalCategoryStruct.tensorUnit M)).app X)
        ((F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor n).hom).app X)) =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor C C)).obj ((F.obj n).obj X))
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.gt_of_neg_of_infinitesimal : ∀ {x : ℝ*}, x.Infinitesimal → ∀ r < 0, ↑r < x
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_inverse : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] [inst_3 : CategoryTheory.BraidedCategory D],
  (CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence C D).inverse =
    CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.map' : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {P : Std.Do.Assertion ps} [inst : Monad m]
  [inst_1 : Std.Do.WPMonad m ps] {α β : Type u} {x : m α} {f : α → β} {Q : Std.Do.PostCond β ps},
  ⦃P⦄ x ⦃(fun a => Q.1 (f a), Q.2)⦄ → ⦃P⦄ (f <$> x) ⦃Q⦄
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.coe_zero : ↑0 = 0