mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.parseFirstByte_eq_done_of_utf8DecodeChar?_eq_some : ∀ {b : ByteArray} {i : ℕ} {c : Char},
  b.utf8DecodeChar? i = some c →
    c.utf8Size = 1 →
      ∀ (h' : i < b.size), ByteArray.utf8DecodeChar?.parseFirstByte b[i] = ByteArray.utf8DecodeChar?.FirstByte.done
-- Aesop.Search.SearchM
Aesop.SearchM.instMonad : {Q : Type} → [inst : Aesop.Queue Q] → Monad (Aesop.SearchM Q)
-- Mathlib.Algebra.Group.Units.Defs
Units.instRepr.eq_1 : ∀ {α : Type u} [inst : Monoid α] [inst_1 : Repr α], Units.instRepr = { reprPrec := reprPrec ∘ Units.val }
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_sub_one' : ∀ {y : ℝ}, y - 1 ≠ 0 → ∀ (x : NNReal), x ^ (y - 1) = x ^ y / x
-- Mathlib.Combinatorics.Quiver.Path.Vertices
Quiver.Path.vertices_ne_nil : ∀ {V : Type u_1} [inst : Quiver V] {a b : V} (p : Quiver.Path a b), p.vertices ≠ []
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
/-- *Dirichlet's approximation theorem:*
For any real number `ξ` and positive natural `n`, there are integers `j` and `k`,
with `0 < k ≤ n` and `|k*ξ - j| ≤ 1/(n+1)`.

See also `Real.exists_nat_abs_mul_sub_round_le`.  -/
Real.exists_int_int_abs_mul_sub_le : ∀ (ξ : ℝ) {n : ℕ}, 0 < n → ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- **Cauchy integral formula** for the value at the center of a disc. If `f : ℂ → E` is continuous on a
closed disc of radius `R` and center `c`, and is complex differentiable at all but countably many
points of its interior, then the integral $\oint_{|z-c|=R} \frac{f(z)}{z-c}\,dz$ is equal to
`2πi • f c`.
 -/
Complex.circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {R : ℝ},
  0 < R →
    ∀ {f : ℂ → E} {c : ℂ} {s : Set ℂ},
      s.Countable →
        ContinuousOn f (Metric.closedBall c R) →
          (∀ z ∈ Metric.ball c R \ s, DifferentiableAt ℂ f z) →
            ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z = (2 * ↑Real.pi * Complex.I) • f c
-- Lean.Meta.Match.MVarRenaming
Lean.Meta.MVarRenaming.mk.injEq : ∀ (map map_1 : Lean.MVarIdMap Lean.MVarId), ({ map := map } = { map := map_1 }) = (map = map_1)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.PreInstance.mk.injEq : ∀ (proof : Lean.Expr) (assignment : Array Lean.Expr) (proof_1 : Lean.Expr) (assignment_1 : Array Lean.Expr),
  ({ proof := proof, assignment := assignment } = { proof := proof_1, assignment := assignment_1 }) =
    (proof = proof_1 ∧ assignment = assignment_1)
-- Mathlib.Algebra.Order.BigOperators.Expect
Finset.exists_le_of_expect_le : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [IsOrderedCancelAddMonoid α]
  [inst_3 : Module ℚ≥0 α] [PosSMulStrictMono ℚ≥0 α] {a : α} {s : Finset ι} {f : ι → α},
  s.Nonempty → (s.expect fun i => f i) ≤ a → ∃ x ∈ s, f x ≤ a
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.sum_zero : ∀ {M : Type u_3} [inst : AddCommMonoid M], Multiset.sum 0 = 0
-- Mathlib.LinearAlgebra.DFinsupp
LinearMap.map_dfinsuppSumAddHom : ∀ {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} {ι : Type u_11} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [inst_4 : Module R M]
  [inst_5 : Module R₂ M₂] {γ : ι → Type u_12} [inst_6 : DecidableEq ι] [inst_7 : (i : ι) → AddZeroClass (γ i)]
  (f : M →ₛₗ[σ₁₂] M₂) {t : Π₀ (i : ι), γ i} {g : (i : ι) → γ i →+ M},
  f ((DFinsupp.sumAddHom g) t) = (DFinsupp.sumAddHom fun i => f.toAddMonoidHom.comp (g i)) t
-- Mathlib.MeasureTheory.SetAlgebra
/-- The algebra of sets generated by a family of sets is an algebra of sets.  -/
MeasureTheory.isSetAlgebra_generateSetAlgebra : ∀ {α : Type u_1} {𝒜 : Set (Set α)}, MeasureTheory.IsSetAlgebra (MeasureTheory.generateSetAlgebra 𝒜)
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteSAsRing : {α : Type u_1} →
  [inst : Lean.Grind.Semiring α] →
    Lean.Grind.CommRing.Context α → Lean.Grind.CommRing.Expr → Lean.Grind.Ring.OfSemiring.Q α
-- Mathlib.Analysis.Complex.Order
Complex.real_le_real : ∀ {x y : ℝ}, ↑x ≤ ↑y ↔ x ≤ y
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.mulRight.congr_simp : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : SeparatelyContinuousMul G] (a a_1 : G),
  a = a_1 → Homeomorph.mulRight a = Homeomorph.mulRight a_1
-- Lean.Parser.Command
Lean.Parser.Command.whereStructInst.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.IsConj.ext_iff : ∀ {K : Type u_1} [inst : Field K] {k : Type u_2} [inst_1 : Field k] [inst_2 : Algebra k K] {φ : K →+* ℂ}
  {σ₁ σ₂ : Gal(K/k)}, NumberField.ComplexEmbedding.IsConj φ σ₁ → (σ₁ = σ₂ ↔ NumberField.ComplexEmbedding.IsConj φ σ₂)
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
WeakSpace.instContinuousSMul : ∀ {𝕜 : Type u_2} {E : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E]
  [ContinuousSMul 𝕜 𝕜], ContinuousSMul 𝕜 (WeakSpace 𝕜 E)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.insertMany_list_equiv_congr : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      (↑m₁).Equiv ↑m₂ →
        ∀ {l : List (α × β)},
          (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m₁ l)).Equiv
            ↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m₂ l)
-- Mathlib.Topology.DenseEmbedding
IsDenseInducing.closure_image_mem_nhds : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β} {s : Set α}
  {a : α}, IsDenseInducing i → s ∈ nhds a → closure (i '' s) ∈ nhds (i a)
-- Mathlib.GroupTheory.Congruence.Hom
/-- Given a surjective multiplicative-preserving function `f` whose kernel is contained in a
congruence relation `c`, the congruence relation on `f`'s codomain defined by '`x ≈ y` iff the
elements of `f⁻¹(x)` are related to the elements of `f⁻¹(y)` by `c`.'  -/
Con.mapOfSurjective : {M : Type u_1} →
  {N : Type u_2} →
    {F : Type u_4} →
      [inst : Mul M] →
        [inst_1 : Mul N] →
          [inst_2 : FunLike F M N] →
            [inst_3 : MulHomClass F M N] → {c : Con M} → (f : F) → Con.ker f ≤ c → Function.Surjective ⇑f → Con N
-- Init.Data.Nat.Basic
Nat.le.intro : ∀ {n m k : ℕ}, n + k = m → n ≤ m
-- Mathlib.GroupTheory.IsSubnormal
/-- A subnormal subgroup of a simple group is either trivial or the whole group.  -/
Subgroup.IsSubnormal.eq_bot_or_top_of_isSimpleGroup : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, IsSimpleGroup G → H.IsSubnormal → H = ⊥ ∨ H = ⊤
-- Mathlib.NumberTheory.Height.Basic
Height.logHeight₁_div_eq_logHeight : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x y : K),
  Height.logHeight₁ (x / y) = Height.logHeight ![x, y]
-- Mathlib.Data.Multiset.Defs
Multiset.coe_eq_coe : ∀ {α : Type u_1} {l₁ l₂ : List α}, ↑l₁ = ↑l₂ ↔ l₁.Perm l₂
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Mathlib.Meta.NormNum.IsNat.nnreal_rpow_eq_nnreal_pow : ∀ {b : ℝ} {n : ℕ}, Mathlib.Meta.NormNum.IsNat b n → ∀ (a : NNReal), a ^ b = a ^ n
-- Mathlib.Order.BooleanAlgebra.Defs
Bool.compl_eq_bnot : compl = not
-- Init.Prelude
/-- `True` is a proposition and has only an introduction rule, `True.intro : True`.
In other words, `True` is simply true, and has a canonical proof, `True.intro`
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)
 -/
True : Prop
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.trivial_mon_mul : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.MonObj.mul =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
-- Init.Data.String.Basic
String.Slice.utf8ByteSize_sliceTo : ∀ {s : String.Slice} {pos : s.Pos}, (s.sliceTo pos).utf8ByteSize = pos.offset.byteIdx
-- Lean.Util.CollectFVars
Lean.CollectFVars.visit : Lean.Expr → Lean.CollectFVars.Visitor
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.uniformContinuous_toSnowflaking : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : UniformSpace X],
  UniformContinuous ⇑Metric.Snowflaking.toSnowflaking
-- Mathlib.Topology.ContinuousOn
/-- **Alias** of `continuousOn_union_iff_of_isClosed`.

---

A function is continuous on two closed sets iff it is also continuous on their union.  -/
continouousOn_union_iff_of_isClosed : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s t : Set α} {f : α → β},
  IsClosed s → IsClosed t → (ContinuousOn f (s ∪ t) ↔ ContinuousOn f s ∧ ContinuousOn f t)
-- Mathlib.Topology.Algebra.OpenSubgroup
AddSubgroup.isOpen_of_mem_nhds : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousAdd G] (H : AddSubgroup G)
  {g : G}, ↑H ∈ nhds g → IsOpen ↑H
-- Mathlib.Analysis.Calculus.Deriv.Comp
fderivWithin_comp_derivWithin : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : 𝕜 → F} (x : 𝕜)
  {s : Set 𝕜} {l : F → E} {t : Set F},
  DifferentiableWithinAt 𝕜 l t (f x) →
    DifferentiableWithinAt 𝕜 f s x →
      Set.MapsTo f s t → derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x)) (derivWithin f s x)
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.ker_restrict_eq_of_codisjoint : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p q : Submodule R M},
  Codisjoint p q →
    ∀ {B : LinearMap.BilinForm R M},
      (∀ x ∈ p, ∀ y ∈ q, (B x) y = 0) → LinearMap.ker (B.restrict p) = Submodule.comap p.subtype (LinearMap.ker B)
-- Mathlib.Data.Multiset.ZeroCons
Multiset.singleton_ne_zero : ∀ {α : Type u_1} (a : α), {a} ≠ 0
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_alter_le_size : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : Option β → Option β}, m.WF → (m.alter k f).size ≤ m.size + 1
-- Mathlib.Analysis.InnerProductSpace.Calculus
contDiff_norm_sq : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {n : WithTop ℕ∞}, ContDiff ℝ n fun x => ‖x‖ ^ 2
-- Mathlib.GroupTheory.GroupExtension.Basic
GroupExtension.Equiv.ofMonoidHom.eq_1 : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {E : Type u_3} [inst_2 : Group E]
  {S : GroupExtension N E G} {E' : Type u_4} [inst_3 : Group E'] {S' : GroupExtension N E' G} (f : E →* E')
  (comp_inl : f.comp S.inl = S'.inl) (rightHom_comp : S'.rightHom.comp f = S.rightHom),
  GroupExtension.Equiv.ofMonoidHom f comp_inl rightHom_comp =
    { toFun := (↑f).toFun,
      invFun := fun e' =>
        have e := Function.surjInv ⋯ (S'.rightHom e');
        e * S.inl (Function.invFun (⇑S'.inl) ((f e)⁻¹ * e')),
      left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, inl_comm := ⋯, rightHom_comm := ⋯ }
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ReferenceContext : Type
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RocSlice : (α : Type u_1) → (α → Type u_2) → [Ord α] → Type (max u_2 u_1)
-- Lean.Meta.Tactic.TryThis
/-- This is a code action provider that looks for `TryThisInfo` nodes and supplies a code action to
apply the replacement.
 -/
_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider : Lean.Server.CodeActionProvider
-- Std.Data.HashSet.Lemmas
Std.HashSet.isEmpty_eq_size_eq_zero : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α}, m.isEmpty = (m.size == 0)
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- **Alias** of `CategoryTheory.CardinalDirectedPoset.isCardinalPresentable_iff`. -/
CategoryTheory.CardinalFilteredPoset.isCardinalPresentable_iff : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ) {κ' : Cardinal.{u}}
  [inst_1 : Fact κ'.IsRegular], κ ≤ κ' → (CategoryTheory.IsCardinalPresentable J κ' ↔ HasCardinalLT (↑J.obj) κ')
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.DefaultConsumers.forIn_eq : ∀ {γ : Type x} {α β : Type w} {m : Type w → Type w'} {n : Type x → Type x'} [inst : Monad n]
  [inst_1 : Std.Iterator α m β] {lift : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ}
  {plausible_forInStep : β → γ → ForInStep γ → Prop} {it : Std.IterM m β} {init : γ}
  {f : (b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (plausible_forInStep b c))},
  Std.IteratorLoop.forIn lift γ plausible_forInStep it init f =
    Std.IterM.DefaultConsumers.forIn' lift γ plausible_forInStep it init it.IsPlausibleIndirectOutput ⋯ f
-- Init.Data.Nat.Gcd
Nat.gcd_self : ∀ (n : ℕ), n.gcd n = n
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.map_ne_zero : ∀ {R : Type u} {S : Type v} [inst : Ring R] [IsSimpleRing R] [inst_2 : Semiring S] [Nontrivial S] {p : Polynomial R}
  {f : R →+* S}, p ≠ 0 → Polynomial.map f p ≠ 0
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapIso_functor_obj_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T T' : D} {S : CategoryTheory.Functor C D} (i : T ≅ T')
  (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)),
  ((CategoryTheory.CostructuredArrow.mapIso i).functor.obj X).hom = CategoryTheory.CategoryStruct.comp X.hom i.hom
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.toRightFun.eq_1 : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {T : Set G} (hT : Subgroup.IsComplement (↑H) T),
  hT.toRightFun = ⇑hT.rightQuotientEquiv ∘ Quotient.mk''
-- Mathlib.Geometry.Manifold.HasGroupoid
_private.Mathlib.Geometry.Manifold.HasGroupoid.0.restr_mem_maximalAtlas_aux1 : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  (G : StructureGroupoid H) [ClosedUnderRestriction G] {e e' : OpenPartialHomeomorph M H},
  e ∈ StructureGroupoid.maximalAtlas M G → e' ∈ atlas H M → ∀ {s : Set M}, IsOpen s → (e.restr s).symm.trans e' ∈ G
-- Mathlib.Algebra.MonoidAlgebra.Support
/-- An element of `k[G]` is in the subalgebra generated by its support.  -/
MonoidAlgebra.mem_span_support_coeff : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : MulOneClass G] (f : MonoidAlgebra k G),
  f ∈ Submodule.span k (⇑(MonoidAlgebra.of k G) '' ↑f.coeff.support)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.associator_naturality_left_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d)
  {Z : a ⟶ d} (h_1 : CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g h) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η g) h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f' g h).hom h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.comp g h)) h_1)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
groupHomology.inhomogeneousChains.d_single : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (n : ℕ) (g : Fin (n + 1) → G) (a : ↑A),
  ((CategoryTheory.ConcreteCategory.hom (groupHomology.inhomogeneousChains.d A n)) fun₀ | g => a) =
    (fun₀ | fun i => g i.succ => (A.ρ (g 0)⁻¹) a) +
      ∑ j, (-1) ^ (↑j + 1) • fun₀ | j.contractNth (fun x1 x2 => x1 * x2) g => a
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- the composition of the two directions of a homotopy equivalence is
homotopic to the identity of the target  -/
CategoryTheory.ShortComplex.HomotopyEquiv.homotopyInvHomId : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (self : S₁.HomotopyEquiv S₂) →
          CategoryTheory.ShortComplex.Homotopy (CategoryTheory.CategoryStruct.comp self.inv self.hom)
            (CategoryTheory.CategoryStruct.id S₂)
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.instLEQOfOrderedAdd : {α : Type u} →
  [inst : Lean.Grind.NatModule α] →
    [inst_1 : LE α] →
      [inst_2 : Std.IsPreorder α] → [Lean.Grind.OrderedAdd α] → LE (Lean.Grind.IntModule.OfNatModule.Q α)
-- Batteries.Data.BitVec.Lemmas
BitVec.toFin_ofFnLEAux : ∀ {n : ℕ} (m : ℕ) (f : Fin n → Bool), (BitVec.ofFnLEAux m f).toFin = Fin.ofNat (2 ^ m) (Nat.ofBits f)
-- Mathlib.Data.Finset.Sups
Finset.compls.eq_1 : ∀ {α : Type u_2} [inst : BooleanAlgebra α], Finset.compls = Finset.map { toFun := compl, inj' := ⋯ }
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_le_pow₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀],
  1 ≤ a → ∀ {n : ℕ}, 1 ≤ a ^ n
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
CategoryTheory.LocallyDiscrete.eqToHom_toLoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {a b : C} (h : a = b),
  (CategoryTheory.eqToHom h).toLoc = CategoryTheory.eqToHom ⋯
-- Init.Data.Int.Linear
Int.Internal.Linear.norm_dvd_gcd_cert : ℤ → Int.Internal.Linear.Expr → ℤ → Int.Internal.Linear.Poly → ℤ → Bool
-- Mathlib.Algebra.Colimit.Ring
Ring.DirectLimit.ringEquiv_of : ∀ {ι : Type u_1} [inst : Preorder ι] (G : ι → Type u_2) [inst_1 : (i : ι) → CommRing (G i)]
  (f' : (i j : ι) → i ≤ j → G i →+* G j) [inst_2 : DirectedSystem G fun i j h => ⇑(f' i j h)]
  [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι] {i : ι} {g : G i},
  (Ring.DirectLimit.ringEquiv G f') ((Ring.DirectLimit.of G (fun x1 x2 x3 => ⇑(f' x1 x2 x3)) i) g) = ⟦⟨i, g⟩⟧
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_eq_of_le : ∀ {n : ℤ} {m : ℕ}, -(↑m / 2) ≤ n → n < (↑m + 1) / 2 → n.bmod m = n
-- Mathlib.Topology.Order
isClosed_coinduced : ∀ {α : Type u_1} {β : Type u_2} {t : TopologicalSpace α} {s : Set β} {f : α → β}, IsClosed s ↔ IsClosed (f ⁻¹' s)
-- Mathlib.Data.Fintype.Lattice
Finite.exists_max : ∀ {α : Type u_2} {β : Type u_3} [Finite α] [Nonempty α] [inst : LinearOrder β] (f : α → β), ∃ x₀, ∀ (x : α), f x ≤ f x₀
-- Lean.Message
/-- Checks if either of `reported` or `unreported` contains an error, i.e. whether the current command
has errored yet.
 -/
Lean.MessageLog.hasErrors : Lean.MessageLog → Bool
-- Mathlib.Topology.Algebra.Group.Basic
/-- A subgroup `S` of an additive topological group `G` acts on `G` properly
discontinuously on the left, if it is discrete in the sense that `S ∩ K` is finite for all compact
`K`. (See also `DiscreteTopology`.)  -/
AddSubgroup.properlyDiscontinuousVAdd_of_tendsto_cofinite : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] (S : AddSubgroup G),
  Filter.Tendsto (⇑S.subtype) Filter.cofinite (Filter.cocompact G) → ProperlyDiscontinuousVAdd (↥S) G
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteSAsRing.eq_2 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (k : ℕ),
  Lean.Grind.CommRing.Expr.denoteSAsRing ctx (Lean.Grind.CommRing.Expr.natCast k) = OfNat.ofNat k
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.of_postcomp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C)
  {W' : CategoryTheory.MorphismProperty C} [W.HasOfPostcompProperty W'] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
  W' g → W (CategoryTheory.CategoryStruct.comp f g) → W f
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Under.map_comp : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) [inst_1 : Q.IsMultiplicative] {X Y Z : T}
  [inst_2 : P.IsStableUnderComposition] {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g),
  CategoryTheory.MorphismProperty.Under.map Q ⋯ =
    (CategoryTheory.MorphismProperty.Under.map Q hg).comp (CategoryTheory.MorphismProperty.Under.map Q hf)
-- Mathlib.LinearAlgebra.AffineSpace.Slope
MonotoneOn.slope_nonneg : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E]
  [inst_3 : LinearOrder k] [IsStrictOrderedRing k] [inst_5 : PartialOrder E] [IsOrderedAddMonoid E] [PosSMulMono k E]
  {f : k → E} {x y : k} {s : Set k}, MonotoneOn f s → x ∈ s → y ∈ s → 0 ≤ slope f x y
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
_private.Mathlib.RingTheory.Coalgebra.CoassocSimps.0.CoassocSimps.«term_⊗ₘ_» : Lean.TrailingParserDescr
-- Mathlib.FieldTheory.AbelRuffini
/-- Inductive definition of solvable by radicals  -/
IsSolvableByRad : (F : Type u_1) → {E : Type u_2} → [inst : Field F] → [inst_1 : Field E] → [Algebra F E] → E → Prop
-- Mathlib.Topology.Order.OrderClosed
ge_of_tendsto : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIciTopology α] {f : β → α}
  {a b : α} {x : Filter β} [hx : x.NeBot], Filter.Tendsto f x (nhds a) → (∀ᶠ (c : β) in x, b ≤ f c) → b ≤ a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_inter!_le_size_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → (m₁.inter! m₂).size ≤ m₁.size
-- Mathlib.Order.Category.BddOrd
BddOrd.hom_comp : ∀ {X Y Z : BddOrd} (f : X ⟶ Y) (g : Y ⟶ Z),
  BddOrd.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (BddOrd.Hom.hom g).comp (BddOrd.Hom.hom f)
-- Mathlib.Topology.UniformSpace.UniformConvergence
UniformCauchySeqOnFilter.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] (F : ι → α → β) (p : Filter ι) (p' : Filter α),
  UniformCauchySeqOnFilter F p p' =
    ∀ u ∈ uniformity β, ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', (F m.1.1 m.2, F m.1.2 m.2) ∈ u
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.ExactFunctor.whiskeringRight_obj_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : D ⥤ₑ E) {X Y : C ⥤ₑ D} (f : X ⟶ Y),
  ((CategoryTheory.ExactFunctor.whiskeringRight C D E).obj F).map f =
    CategoryTheory.ObjectProperty.homMk (CategoryTheory.Functor.whiskerRight f.hom F.obj)
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
/-- The natural map from `n`-cocycles to `n`th continuous cohomology for a `k`-linear
`G`-representation `A`.  -/
ContinuousCohomology.π : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Ring k] →
      [inst_1 : Group G] →
        [inst_2 : TopologicalSpace k] →
          [inst_3 : TopologicalSpace G] →
            [inst_4 : IsTopologicalGroup G] →
              (A : TopRep k G) →
                (n : ℕ) →
                  HomologicalComplex.cycles A.homogeneousCochains n ⟶
                    HomologicalComplex.homology A.homogeneousCochains n
-- Mathlib.Logic.Relation
Relation.symmGen_swap_apply : ∀ {α : Type u_1} {a b : α} (r : α → α → Prop), Relation.SymmGen (Function.swap r) a b ↔ Relation.SymmGen r a b
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- If a function has a Taylor series at order at least `1`, then the term of order `1` of this
series is a derivative of `f`.  -/
HasFTaylorSeriesUpTo.hasFDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpTo n f p → n ≠ 0 → ∀ (x : E), HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) x