mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
lineDeriv_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {x v : E},
  lineDeriv 𝕜 f x (-v) = -lineDeriv 𝕜 f x v
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.termSoln : Lean.ParserDescr
-- Mathlib.MeasureTheory.Group.LIntegral
MeasureTheory.lintegral_div_right_eq_self : ∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : Group G] [MeasurableMul G]
  [μ.IsMulRightInvariant] (f : G → ENNReal) (g : G), ∫⁻ (x : G), f (x / g) ∂μ = ∫⁻ (x : G), f x ∂μ
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.shiftEquiv'.eq_1 : ∀ (C : Type u) {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddGroup A]
  [inst_2 : CategoryTheory.HasShift C A] (i j : A) (h : i + j = 0),
  CategoryTheory.shiftEquiv' C i j h =
    { functor := CategoryTheory.shiftFunctor C i, inverse := CategoryTheory.shiftFunctor C j,
      unitIso := (CategoryTheory.shiftFunctorCompIsoId C i j h).symm,
      counitIso := CategoryTheory.shiftFunctorCompIsoId C j i ⋯, functor_unitIso_comp := ⋯ }
-- Mathlib.AlgebraicGeometry.Morphisms.FlatRank
AlgebraicGeometry.Scheme.Hom.finrank_of_isPullback : ∀ {P X Y Z : AlgebraicGeometry.Scheme} (fst : P ⟶ X) (snd : P ⟶ Y) (f : X ⟶ Z) (g : Y ⟶ Z),
  CategoryTheory.IsPullback fst snd f g →
    ∀ [AlgebraicGeometry.Flat f] [AlgebraicGeometry.IsFinite f] (y : ↥Y),
      AlgebraicGeometry.Scheme.Hom.finrank snd y = AlgebraicGeometry.Scheme.Hom.finrank f (g y)
-- Mathlib.CategoryTheory.Limits.Final
/-- For the full subcategory induced by an object property `P` on `C`, to show initiality of
the inclusion functor it is enough to consider arrows to objects outside of the subcategory.  -/
CategoryTheory.ObjectProperty.initial_ι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.ObjectProperty C),
  (∀ (d : C), ¬P d → CategoryTheory.IsConnected (CategoryTheory.CostructuredArrow P.ι d)) → P.ι.Initial
-- Init.System.IO
/-- The result of running a process to completion.
 -/
IO.Process.Output : Type
-- Mathlib.CategoryTheory.Action.Limits
Action.instAbelian : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} → [inst_1 : Monoid G] → [CategoryTheory.Abelian V] → CategoryTheory.Abelian (Action V G)
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.getRepr.match_1.splitter : {n : ℕ} →
  (motive : Option (Fin n) → Sort u_1) →
    (x : Option (Fin n)) → ((y : Fin n) → x = some y → motive (some y)) → (x = none → motive none) → motive x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.ofRepresentableBy.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (X : C)
  (F : CategoryTheory.Functor Cᵒᵖ GrpCat) (α : (F.comp (CategoryTheory.forget GrpCat)).RepresentableBy X),
  CategoryTheory.GrpObj.ofRepresentableBy X F α =
    { toMonObj := CategoryTheory.MonObj.ofRepresentableBy X (F.comp (CategoryTheory.forget₂ GrpCat MonCat)) α,
      inv := α.homEquiv'.symm (α.homEquiv (CategoryTheory.CategoryStruct.id X))⁻¹, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_obj₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (i : EInt) (j : C),
  ((t.eTriangleLTGE.obj i).obj j).obj₃ = (t.eTruncGE.obj i).obj j
-- Mathlib.Topology.Bases
/-- If a family of open sets `s` is such that every open neighbourhood contains some
member of `s`, then `s` is a topological basis.  -/
TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds : ∀ {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)},
  (∀ u ∈ s, IsOpen u) →
    (∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v ∈ s, a ∈ v ∧ v ⊆ u) → TopologicalSpace.IsTopologicalBasis s
-- Mathlib.Analysis.Calculus.Deriv.Abs
differentiableWithinAt_abs_pos : ∀ (s : Set ℝ) {x : ℝ}, 0 < x → DifferentiableWithinAt ℝ (fun x => |x|) s x
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.δ_comp_δ_self' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {j : Fin (n + 3)} {i : Fin (n + 2)},
  j = i.castSucc →
    CategoryTheory.CategoryStruct.comp (X.δ j) (X.δ i) = CategoryTheory.CategoryStruct.comp (X.δ i.succ) (X.δ i)
-- Lean.Meta.Basic
Lean.Meta.modifyDefEqPermCache : (Lean.Meta.DefEqCache → Lean.Meta.DefEqCache) → Lean.MetaM Unit
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rcc_eq_singleton_iff : ∀ {k m n : ℤ}, (m...=n).toList = [k] ↔ n = m ∧ m = k
-- Mathlib.ModelTheory.DirectLimit
/-- The direct limit of a directed system is the structures glued together along the embeddings.  -/
FirstOrder.Language.DirectLimit : {L : FirstOrder.Language} →
  {ι : Type v} →
    [inst : Preorder ι] →
      (G : ι → Type w) →
        [inst_1 : (i : ι) → L.Structure (G i)] →
          (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) →
            [DirectedSystem G fun i j h => ⇑(f i j h)] → [IsDirectedOrder ι] → Type (max v w)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- The `covolume` of an action of `G` on `α` the volume of some fundamental domain, or `0` if
none exists.  -/
MeasureTheory.covolume : (G : Type u_6) →
  (α : Type u_7) →
    [One G] →
      [SMul G α] →
        [inst : MeasurableSpace α] → autoParam (MeasureTheory.Measure α) MeasureTheory.covolume._auto_1 → ENNReal
-- Lean.Parser.Types
Lean.Parser.FirstTokens.optTokens.sizeOf_spec : ∀ (a : List Lean.Parser.Token), sizeOf (Lean.Parser.FirstTokens.optTokens a) = 1 + sizeOf a
-- Mathlib.RingTheory.Ideal.IsPrincipal
/-- The equivalence between `Associates R` and the principal ideals of `R` defined by sending the
class of `x` to the principal ideal generated by `x`.  -/
Ideal.associatesEquivIsPrincipal : (R : Type u_1) → [inst : CommRing R] → [IsDomain R] → Associates R ≃ { I // Submodule.IsPrincipal I }
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.congr_fun : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  {φ₁ φ₂ : A →ₗc[R] B}, φ₁ = φ₂ → ∀ (x : A), φ₁ x = φ₂ x
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
/-- Consider differentiable maps `v : M → E₁` and `w : M → E₂` to vector bundles, over a base map
`b : M → B`, and bilinear maps `ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m)` depending smoothly on `m`.
One can apply `ψ  m` to `v m` and `w m`, and the resulting map is differentiable.  -/
MDifferentiable.clm_bundle_apply₂ : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {F₃ : Type u_5} {M : Type u_6}
  [inst : NontriviallyNormedField 𝕜] {E₁ : B → Type u_7} [inst_1 : (x : B) → AddCommGroup (E₁ x)]
  [inst_2 : (x : B) → Module 𝕜 (E₁ x)] [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_6 : (x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_8}
  [inst_7 : (x : B) → AddCommGroup (E₂ x)] [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂]
  [inst_10 : NormedSpace 𝕜 F₂] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {E₃ : B → Type u_9} [inst_13 : (x : B) → AddCommGroup (E₃ x)]
  [inst_14 : (x : B) → Module 𝕜 (E₃ x)] [inst_15 : NormedAddCommGroup F₃] [inst_16 : NormedSpace 𝕜 F₃]
  [inst_17 : TopologicalSpace (Bundle.TotalSpace F₃ E₃)] [inst_18 : (x : B) → TopologicalSpace (E₃ x)] {EB : Type u_10}
  [inst_19 : NormedAddCommGroup EB] [inst_20 : NormedSpace 𝕜 EB] {HB : Type u_11} [inst_21 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_22 : TopologicalSpace B] [inst_23 : ChartedSpace HB B] {EM : Type u_12}
  [inst_24 : NormedAddCommGroup EM] [inst_25 : NormedSpace 𝕜 EM] {HM : Type u_13} [inst_26 : TopologicalSpace HM]
  {IM : ModelWithCorners 𝕜 EM HM} [inst_27 : TopologicalSpace M] [inst_28 : ChartedSpace HM M]
  [inst_29 : FiberBundle F₁ E₁] [inst_30 : VectorBundle 𝕜 F₁ E₁] [inst_31 : FiberBundle F₂ E₂]
  [inst_32 : VectorBundle 𝕜 F₂ E₂] [inst_33 : FiberBundle F₃ E₃] [inst_34 : VectorBundle 𝕜 F₃ E₃] {b : M → B}, ⋯
-- Lean.Compiler.IR.Basic
Lean.IR.LitVal.str.injEq : ∀ (v v_1 : String), (Lean.IR.LitVal.str v = Lean.IR.LitVal.str v_1) = (v = v_1)
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- If `A ≃g H` and `B ≃g G` then `B` is `A`-free if and only if `G` is `H`-free.  -/
SimpleGraph.free_congr : ∀ {V : Type u_1} {W : Type u_2} {α : Type u_4} {β : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W}
  {A : SimpleGraph α} {B : SimpleGraph β} (e₁ : A ≃g H) (e₂ : B ≃g G), A.Free B ↔ H.Free G
-- Lean.Expr
Lean.Expr.proj.injEq : ∀ (typeName : Lean.Name) (idx : ℕ) (struct : Lean.Expr) (typeName_1 : Lean.Name) (idx_1 : ℕ) (struct_1 : Lean.Expr),
  (Lean.Expr.proj typeName idx struct = Lean.Expr.proj typeName_1 idx_1 struct_1) =
    (typeName = typeName_1 ∧ idx = idx_1 ∧ struct = struct_1)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder
/-- A functor `G : C ⥤ D` satisfies `PreservesWellOrderContinuousOfShape J G`
if for any limit element `j` in the preordered type `J`, the functor `G`
preserves colimits of shape `Set.Iio j`.  -/
CategoryTheory.Limits.PreservesWellOrderContinuousOfShape : {C : Type u} →
  {D : Type u'} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Category.{v', u'} D] → (J : Type w) → [LinearOrder J] → CategoryTheory.Functor C D → Prop
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.symm : ∀ {M : Type u_1} [inst : Monoid M] {x y : M}, Associated x y → Associated y x
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.coe_eq_one : ∀ {z : Complex.UnitClosedDisc}, ↑z = 1 ↔ z = 1
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr.eq_4 : ∀ (p : Turing.PartrecToTM2.Γ' → Bool) (k : Turing.PartrecToTM2.K') (q : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.clear p k q) =
    Turing.PartrecToTM2.pop' k
      (Turing.TM2.Stmt.branch (fun s => s.elim true p) (Turing.TM2.Stmt.goto fun x => q)
        (Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.Λ'.clear p k q))
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreZeroHypercover.isoMk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S}
  (s₀ : E.I₀ ≃ F.I₀) (h₀ h₀_1 : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (e_h₀ : h₀ = h₀_1)
  (w₀ : ∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i),
  CategoryTheory.PreZeroHypercover.isoMk s₀ h₀ w₀ = CategoryTheory.PreZeroHypercover.isoMk s₀ h₀_1 ⋯
-- Mathlib.LinearAlgebra.Transvection.Generation
LinearEquiv.le_one_add_finrank_fixedSubmodule_mul_dilatransvection : ∀ {K : Type u_1} [inst : DivisionRing K] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [Module.Finite K V] (e f : V ≃ₗ[K] V),
  f ∈ LinearEquiv.dilatransvections K V →
    Module.finrank K ↥(↑e).fixedSubmodule ≤ 1 + Module.finrank K ↥(↑(e * f)).fixedSubmodule
-- Mathlib.Algebra.Order.Ring.Abs
abs_le_of_sq_le_sq : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α},
  a ^ 2 ≤ b ^ 2 → 0 ≤ b → |a| ≤ b
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- The functor `Localization W ⥤ E` that is induced by a functor `C ⥤ E` which inverts `W`,
when `W` has a left calculus of fractions.  -/
CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget.lift : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} →
      [inst_1 : W.HasLeftCalculusOfFractions] →
        {E : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            (F : CategoryTheory.Functor C E) →
              W.IsInvertedBy F → CategoryTheory.Functor (CategoryTheory.MorphismProperty.LeftFraction.Localization W) E
-- Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
AlgebraicGeometry.Scheme.irreducibleComponentIdeal_def : ∀ (X : AlgebraicGeometry.Scheme) (Z : Set ↥X) (hZ : Z ∈ irreducibleComponents ↥X)
  [inst : AlgebraicGeometry.IsNoetherian X],
  X.irreducibleComponentIdeal Z hZ = AlgebraicGeometry.Scheme.Hom.ker (X.irreducibleComponentOpen Z).ι
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.S.cons.sizeOf_spec : ∀ (a b : Mathlib.Deriving.Encodable.S✝), sizeOf (Mathlib.Deriving.Encodable.S.cons✝ a b) = 1 + sizeOf a + sizeOf b
-- Mathlib.CategoryTheory.Localization.Resolution
/-- a morphism to an object of the form `Φ.functor.obj X₁`  -/
CategoryTheory.LocalizerMorphism.RightResolution.w : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} →
              {X₂ : C₂} → (self : Φ.RightResolution X₂) → X₂ ⟶ Φ.functor.obj self.X₁
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.image_to_eq_image : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c)
  [inst_2 : CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasEqualizers V] {i j : ι},
  c.Rel i j → CategoryTheory.Limits.imageSubobject (C.dTo j) = CategoryTheory.Limits.imageSubobject (C.d i j)
-- Mathlib.Topology.Sheaves.CommRingCat
/-- The (bundled) commutative ring of continuous functions from a topological space
to a topological commutative ring, with pointwise multiplication.  -/
TopCat.continuousFunctions : TopCatᵒᵖ → TopCommRingCat → CommRingCat
-- Mathlib.MeasureTheory.Constructions.Cylinders
/-- A finset `s` such that `t = cylinder s S`. `S` is given by `measurableCylinders.set`.  -/
MeasureTheory.measurableCylinders.finset : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → MeasurableSpace (α i)] →
      {t : Set ((i : ι) → α i)} → t ∈ MeasureTheory.measurableCylinders α → Finset ι
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.min?.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (h_1 : Unit → motive RBTree.RBNode.nil)
  (h_2 : (c : RBTree.RBColor) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c RBTree.RBNode.nil v r))
  (h_3 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c l v r)),
  (match RBTree.RBNode.nil with
    | RBTree.RBNode.nil => h_1 ()
    | RBTree.RBNode.node c RBTree.RBNode.nil v r => h_2 c v r
    | RBTree.RBNode.node c l v r => h_3 c l v r) =
    h_1 ()
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.contLinear_eq_zero_iff_exists_const : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] [inst_9 : TopologicalSpace V]
  [inst_10 : IsTopologicalAddTorsor P] [inst_11 : TopologicalSpace W] [inst_12 : IsTopologicalAddTorsor Q]
  (f : P →ᴬ[R] Q), f.contLinear = 0 ↔ ∃ q, f = ContinuousAffineMap.const R P q
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.inf_comm : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] (a b : CauSeq α abs),
  a ⊓ b = b ⊓ a
-- Init.Omega.Coeffs
Lean.Omega.Coeffs.dot_distrib_left : ∀ (xs ys zs : Lean.Omega.Coeffs), (xs + ys).dot zs = xs.dot zs + ys.dot zs
-- Std.Time.DateTime.PlainDateTime
Std.Time.PlainDateTime.instHAddOffset_3 : HAdd Std.Time.PlainDateTime Std.Time.Minute.Offset Std.Time.PlainDateTime
-- Mathlib.RingTheory.Derivation.Basic
Derivation.instAdd : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Algebra R A] → [inst_4 : Module A M] → [inst_5 : Module R M] → Add (Derivation R A M)
-- Mathlib.Order.WellFounded
acc_iff_isEmpty_descending_chain : ∀ {α : Sort u_1} {r : α → α → Prop} {x : α}, Acc r x ↔ IsEmpty { f // f 0 = x ∧ ∀ (n : ℕ), r (f (n + 1)) (f n) }
-- Std.Http.Protocol.H1
/-- Returns whether the machine should pause after headers waiting for a
`canContinue` decision (`Expect: 100-continue` flow).
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.waitingContinueAfterHeaders : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Bool
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.restrict_isNonloop_iff : ∀ {α : Type u_1} {M : Matroid α} {e : α} {R : Set α}, (M.restrict R).IsNonloop e ↔ M.IsNonloop e ∧ e ∈ R
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- If `R → A → B` is an algebra tower with `A → B` injective,
then if the entire tower is an integral extension so is `R → A`  -/
IsIntegral.tower_bot : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Ring B]
  [inst_3 : Algebra A B] [inst_4 : Algebra R B] [inst_5 : Algebra R A] [IsScalarTower R A B],
  Function.Injective ⇑(algebraMap A B) → ∀ {x : A}, IsIntegral R ((algebraMap A B) x) → IsIntegral R x
-- Init.Data.List.Sublist
List.IsInfix.ne_nil : ∀ {α : Type u_1} {xs ys : List α}, xs <:+: ys → xs ≠ [] → ys ≠ []
-- Mathlib.SetTheory.Cardinal.CountableCover
/-- If a space is eventually covered by a countable family of sets, all with cardinality `a`,
then the cardinality of the space is also `a`.  -/
Cardinal.mk_of_countable_eventually_mem : ∀ {α : Type u} {ι : Type v} {a : Cardinal.{u}} [Countable ι] {f : ι → Set α} {l : Filter ι} [l.NeBot],
  (∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i) → (∀ (i : ι), Cardinal.mk ↑(f i) = a) → Cardinal.mk α = a
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
MulEquiv.toMulEquiv_toContinuousMulEquiv : ∀ {G : Type u} [inst : TopologicalSpace G] {H : Type v} [inst_1 : TopologicalSpace H] [inst_2 : Mul G] [inst_3 : Mul H]
  {e : G ≃* H} (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s), ↑(e.toContinuousMulEquiv he) = e
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Break.runK.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.ElimInfo.mk : Lean.Expr → Lean.Expr → ℕ → Array ℕ → Array Lean.Meta.ElimAltInfo → ℕ → Lean.Meta.ElimInfo
-- Mathlib.NumberTheory.ModularForms.QExpansion
/-- Specialized version of `UpperHalfPlane.hasSum_qExpansion` for modular forms, with many
arguments filled in automatically.  -/
ModularForm.hasSum_qExpansion : ∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F),
  0 < h →
    ∀ {k : ℤ} [ModularFormClass F Γ k] [Fact (IsCusp OnePoint.infty Γ)],
      h ∈ Γ.strictPeriods →
        ∀ (τ : UpperHalfPlane),
          HasSum (fun m => (PowerSeries.coeff m) (UpperHalfPlane.qExpansion h ⇑f) * Function.Periodic.qParam h ↑τ ^ m)
            (f τ)
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivialization.pullback_source : ∀ {B : Type u} {F : Type v} {E : B → Type w₁} {B' : Type w₂} [inst : TopologicalSpace B']
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : TopologicalSpace F] [inst_3 : TopologicalSpace B]
  [inst_4 : ∀ (_b : B), Nonempty (E _b)] {K : Type U} [inst_5 : FunLike K B' B] [inst_6 : ContinuousMapClass K B' B]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) (f : K),
  (e.pullback f).source = Bundle.Pullback.lift ⇑f ⁻¹' e.source
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.comp_measurable : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace β] {x : MeasurableSpace α}
  {x_1 : MeasurableSpace γ} {f : α → β} {g : γ → α},
  MeasureTheory.StronglyMeasurable f → Measurable g → MeasureTheory.StronglyMeasurable (f ∘ g)
-- Init.Data.UInt.Lemmas
USize.add_assoc : ∀ (a b c : USize), a + b + c = a + (b + c)
-- Mathlib.Topology.Compactification.StoneCech
continuous_preStoneCechExtend : ∀ {α : Type u} [inst : TopologicalSpace α] {β : Type v} [inst_1 : TopologicalSpace β] [inst_2 : T2Space β]
  [inst_3 : CompactSpace β] {g : α → β} (hg : Continuous g), Continuous (preStoneCechExtend hg)
-- Init.Data.String.Substring
_private.Init.Data.String.Substring.0.Substring.Raw.takeWhileAux.eq_def : ∀ (s : String) (stopPos : String.Pos.Raw) (p : Char → Bool) (i : String.Pos.Raw),
  Substring.Raw.takeWhileAux s stopPos p i =
    if h : i < stopPos then
      if p (String.Pos.Raw.get s i) = true then
        have this := ⋯;
        Substring.Raw.takeWhileAux s stopPos p (String.Pos.Raw.next s i)
      else i
    else i
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.deleteEdges_fromEdgeSet : ∀ {V : Type u_1} (s t : Set (Sym2 V)), (SimpleGraph.fromEdgeSet s).deleteEdges t = SimpleGraph.fromEdgeSet (s \ t)
-- Mathlib.Control.Functor
/-- If we consider `x : F α` to, in some sense, contain values of type `α`, then
`Liftr r x y` relates `x` and `y` iff (1) `x` and `y` have the same shape and
(2) we can pair values `a` from `x` and `b` from `y` so that `r a b` holds.  -/
Functor.Liftr : {F : Type u → Type v} → [Functor F] → {α : Type u} → (α → α → Prop) → F α → F α → Prop
-- Mathlib.Analysis.Calculus.FDeriv.Bilinear
IsBoundedBilinearMap.fderiv : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {b : E × F → G} (h : IsBoundedBilinearMap 𝕜 b) (p : E × F),
  fderiv 𝕜 b p = h.deriv p
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.exists_eq_of_iSup_eq_of_not_isSuccLimit : ∀ {ι : Type u} [hι : Nonempty ι] (f : ι → Cardinal.{v}),
  BddAbove (Set.range f) → ∀ {c : Cardinal.{v}}, ¬Order.IsSuccLimit c → ⨆ i, f i = c → ∃ i, f i = c
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.coeff_eq_zero_of_lt_natTrailingDegree : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, n < p.natTrailingDegree → p.coeff n = 0
-- Mathlib.Topology.ContinuousMap.Compact
/-- When `α` is compact, the bounded continuous maps `α →ᵇ 𝕜` are
additively equivalent to `C(α, 𝕜)`.
 -/
ContinuousMap.addEquivBoundedOfCompact : (α : Type u_1) →
  (β : Type u_2) →
    [inst : TopologicalSpace α] →
      [CompactSpace α] →
        [inst_2 : PseudoMetricSpace β] →
          [inst_3 : AddMonoid β] → [inst_4 : LipschitzAdd β] → C(α, β) ≃+ BoundedContinuousFunction α β
-- Mathlib.NumberTheory.ModularForms.SlashActions
ModularForm.SL_slash_apply : ∀ {k : ℤ} (f : UpperHalfPlane → ℂ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane),
  SlashAction.map k γ f τ =
    f (γ • τ) *
      UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ ^
        (-k)
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.hom_ext_iff : ∀ {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.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.AddMonObj A] {M N : CategoryTheory.AddMod D A} {f₁ f₂ : M ⟶ N},
  f₁ = f₂ ↔ f₁.hom = f₂.hom