mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.JsonRpc
Lean.JsonRpc.instCoeOutResponseMessageOfToJson : {α : Type u_1} → [Lean.ToJson α] → CoeOut (Lean.JsonRpc.Response α) Lean.JsonRpc.Message
-- Lean.Compiler.InlineAttrs
Lean.Compiler.hasInlineIfReduceAttribute : Lean.Environment → Lean.Name → Bool
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt.ctorAlt.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (info : Lean.Compiler.LCNF.CtorInfo) (code : Lean.Compiler.LCNF.Code pu)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_3),
  sizeOf (Lean.Compiler.LCNF.Alt.ctorAlt info code h) = 1 + sizeOf info + sizeOf code + sizeOf h
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- The category of pointed Galois objects.  -/
CategoryTheory.PreGaloisCategory.PointedGaloisObject.instCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      (F : CategoryTheory.Functor C FintypeCat) →
        CategoryTheory.Category.{u₂, max (max w u₂) u₁} (CategoryTheory.PreGaloisCategory.PointedGaloisObject F)
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracketWithin_const_smul_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {s : Set E} {x : E} {c : 𝕜},
  DifferentiableWithinAt 𝕜 V s x →
    UniqueDiffWithinAt 𝕜 s x → VectorField.lieBracketWithin 𝕜 (c • V) W s x = c • VectorField.lieBracketWithin 𝕜 V W s x
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Algebra.GrothendieckGroup.instCommGroup.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M],
  Algebra.GrothendieckGroup.instCommGroup =
    { toMonoid := inferInstance.toMonoid, toInv := Algebra.GrothendieckGroup.instInv, div := DivInvMonoid.div',
      zpow := zpowRec, div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯,
      mul_comm := ⋯ }
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
/-- The representation of the clifford conjugate (i.e. the reverse of the involute) in the even
subalgebra is just the reverse of the representation.  -/
CliffordAlgebra.coe_toEven_reverse_involute : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (x : CliffordAlgebra Q),
  ↑((CliffordAlgebra.toEven Q) (CliffordAlgebra.reverse (CliffordAlgebra.involute x))) =
    CliffordAlgebra.reverse ↑((CliffordAlgebra.toEven Q) x)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_sub_right₀ : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : Sub β] [MeasurableSub₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), AEMeasurable (f i) μ) → ∀ (i j k : ι), i ≠ j → i ≠ k → ProbabilityTheory.IndepFun (f i) (f j - f k) μ
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.le_chromaticNumber_of_pairwise_adj : ∀ {V : Type u} {G : SimpleGraph V} {n : ℕ} {ι : Type u_1},
  n ≤ Nat.card ι → ∀ (f : ι → V), (Pairwise fun i j => G.Adj (f i) (f j)) → ↑n ≤ G.chromaticNumber
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.acyclic_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c), K.Acyclic ↔ ∀ (i : ι), K.ExactAt i
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.of_le : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] [inst_1 : LE α] [Lean.Grind.ToInt.LE α i]
  {a b : α} {a' b' : ℤ}, ↑a = a' → ↑b = b' → a ≤ b → a' ≤ b'
-- Mathlib.Topology.UniformSpace.Cauchy
Filter.HasBasis.cauchySeq_iff' : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Sort u_1} [Nonempty β] [inst : SemilatticeSup β]
  {u : β → α} {p : γ → Prop} {s : γ → SetRel α α},
  (uniformity α).HasBasis p s → (CauchySeq u ↔ ∀ (i : γ), p i → ∃ N, ∀ n ≥ N, (u n, u N) ∈ s i)
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
/-- A preordering on a ring `R` is a subsemiring of `R` containing all squares,
but not containing `-1`.  -/
RingPreordering : (R : Type u_1) → [CommRing R] → Type u_1
-- Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
SSet.prodStdSimplex.orderHomOfSimplex_coe : ∀ {p q n : ℕ}
  (x :
    (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
          (SSet.stdSimplex.obj { len := q })).obj
      (Opposite.op { len := n }))
  {m : ℕ} (hm : p + q = m) (i : Fin (n + 1)), (SSet.prodStdSimplex.orderHomOfSimplex x hm) i = ⟨↑(x.1 i) + ↑(x.2 i), ⋯⟩
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.lintegral_rnDeriv_mul : ∀ {α : Type u_3} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν],
  μ.AbsolutelyContinuous ν →
    ∀ {f : α → ENNReal}, AEMeasurable f ν → ∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α), f x ∂μ
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.basis_toMatrix_basisFun_mul : ∀ (p : ENNReal) {ι : Type u_2} [inst : Fintype ι] {𝕜 : Type u_5} [inst_1 : SeminormedCommRing 𝕜]
  (b : Module.Basis ι 𝕜 (PiLp p fun x => 𝕜)) (A : Matrix ι ι 𝕜),
  b.toMatrix ⇑(PiLp.basisFun p 𝕜 ι) * A = Matrix.of fun i j => (b.repr (WithLp.toLp p (A.transpose j))) i
-- Mathlib.Algebra.Polynomial.Monomial
Polynomial.ringHom_ext' : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : Semiring S] {f g : Polynomial R →+* S},
  f.comp Polynomial.C = g.comp Polynomial.C → f Polynomial.X = g Polynomial.X → f = g
-- Mathlib.RingTheory.Finiteness.Basic
AlgHom.Finite.comp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : CommRing B] [inst_3 : CommRing C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  {g : B →ₐ[R] C} {f : A →ₐ[R] B}, g.Finite → f.Finite → (g.comp f).Finite
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousMultilinearMap.analyticOn_uncurry_compContinuousLinearMap : ∀ {𝕜 : Type u_1} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] {ι : Type u_5} {Em : ι → Type u_6} {Fm : ι → Type u_7}
  [inst_3 : (i : ι) → NormedAddCommGroup (Em i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (Em i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (Fm i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (Fm i)] [inst_7 : Fintype ι]
  {t : Set (((i : ι) → Fm i →L[𝕜] Em i) × ContinuousMultilinearMap 𝕜 Em G)},
  AnalyticOn 𝕜 (fun p => p.2.compContinuousLinearMap p.1) t
-- Init.Data.Vector.Algebra
Vector.neg_zero : ∀ {α : Type u_1} {n : ℕ} [inst : Zero α] [inst_1 : Neg α], -0 = 0 → -0 = 0
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.mul_div_root_cancel : ∀ {K : Type u_5} [inst : Field K] (f : Polynomial K) [inst_1 : Fact (Irreducible f)],
  (Polynomial.X - Polynomial.C (AdjoinRoot.root f)) *
      (Polynomial.map (AdjoinRoot.of f) f / (Polynomial.X - Polynomial.C (AdjoinRoot.root f))) =
    Polynomial.map (AdjoinRoot.of f) f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.equiv_iff_keysArray_unit_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α Unit cmp}, t₁.Equiv t₂ ↔ t₁.keysArray.Perm t₂.keysArray
-- Mathlib.Data.Finset.Preimage
Finset.map_subset_iff_subset_preimage : ∀ {α : Type u} {β : Type v} {f : α ↪ β} {s : Finset α} {t : Finset β}, Finset.map f s ⊆ t ↔ s ⊆ t.preimage ⇑f ⋯
-- Mathlib.RingTheory.Etale.StandardEtale
/-- `R[X][Y]/⟨f, Yg-1⟩ ≃ (R[X]/f)[1/g]`  -/
StandardEtalePair.equivAwayAdjoinRoot : {R : Type u_1} →
  [inst : CommRing R] → (P : StandardEtalePair R) → P.Ring ≃ₐ[R] Localization.Away ((AdjoinRoot.mk P.f) P.g)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.coe_top : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A], ↑⊤ = Set.univ
-- Init.Data.UInt.Lemmas
USize.toBitVec_ofNat : ∀ (n : ℕ), (OfNat.ofNat n).toBitVec = BitVec.ofNat System.Platform.numBits n
-- Mathlib.Order.Interval.Finset.Defs
Finset.Iic_toDual : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] (a : α),
  Finset.Iic (OrderDual.toDual a) = Finset.map OrderDual.toDual.toEmbedding (Finset.Ici a)
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderivWithin_comp_add_right : ∀ {𝕜 : 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} {s : Set E} (a : E), fderivWithin 𝕜 (fun x => f (x + a)) s x = fderivWithin 𝕜 f (a +ᵥ s) (x + a)
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.instCoeSortType.eq_1 : AddCommGrpCat.instCoeSortType = { coe := AddCommGrpCat.carrier }
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.Adj.symm : ∀ {α : Type u_1} {x y : α} {H : Hypergraph α}, H.Adj x y → H.Adj y x
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.End.addOppositeEquiv_symm_apply_apply : ∀ {M : Type u_2} [inst : AddMonoid M] (m x : M), (AddActionHom.End.addOppositeEquiv.symm m) x = m + x
-- Mathlib.Logic.Equiv.Sum
Equiv.Perm.sumCongr_refl : ∀ {α : Type u_9} {β : Type u_10}, Equiv.Perm.sumCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ⊕ β)
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- Suppose `{ Xᵢ }` is an inverse system of qcqs schemes with affine transition maps.
If `lim Xᵢ` is quasi-affine, then some `Xᵢ` is quasi-affine.  -/
AlgebraicGeometry.Scheme.exists_isQuasiAffine_of_isLimit : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] [∀ (i : I), CompactSpace ↥(D.obj i)]
  [∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)] [c.pt.IsQuasiAffine], ∃ i, (D.obj i).IsQuasiAffine
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.isoWhiskerLeft_hom : ∀ {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 : CategoryTheory.Functor C D)
  {G H : CategoryTheory.Functor D E} (α : G ≅ H), (F.isoWhiskerLeft α).hom = F.whiskerLeft α.hom
-- Batteries.Data.Float.Basic
/-- Converts `f` to a string, including all decimal digits.  -/
Float32.toStringFull : Float32 → String
-- Mathlib.Topology.Algebra.Order.UpperLower
IsUpperSet.closure : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] [HasUpperLowerClosure α] {s : Set α},
  IsUpperSet s → IsUpperSet (closure s)
-- Mathlib.AlgebraicGeometry.GluingOneHypercover
AlgebraicGeometry.Scheme.GlueData.oneHypercover_I₀ : ∀ (D : AlgebraicGeometry.Scheme.GlueData), D.oneHypercover.I₀ = D.J
-- Mathlib.Order.RelIso.Basic
/-- Composition of two relation isomorphisms is a relation isomorphism.  -/
RelIso.trans : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} → {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → r ≃r s → s ≃r t → r ≃r t
-- Std.Time.Duration
Std.Time.instOrdDuration : Ord Std.Time.Duration
-- Mathlib.Topology.Connected.Basic
/-- The iUnion of connected sets indexed by a type with an archimedean successor (like `ℕ` or `ℤ`)
such that any two neighboring sets meet is connected.  -/
IsConnected.iUnion_of_chain : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] [inst_2 : SuccOrder β]
  [IsSuccArchimedean β] [Nonempty β] {s : β → Set α},
  (∀ (n : β), IsConnected (s n)) → (∀ (n : β), (s n ∩ s (Order.succ n)).Nonempty) → IsConnected (⋃ n, s n)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.Iter.foldM_map : ∀ {α β γ δ : Type w} {n : Type w → Type w'} {Pred EPred : Type w} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : Std.Internal.Do.Assertion Pred]
  [inst_4 : Std.Internal.Do.Assertion EPred] [inst_5 : Std.Internal.Do.WPMonad n Pred EPred]
  [inst_6 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {f : β → γ} {g : δ → γ → n δ} {init : δ}
  {it : Std.Iter β} {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄ Std.Iter.foldM (fun d b => g d (f b)) init it ⦃ Q; eQ ⦄ →
    ⦃ P ⦄ Std.Iter.foldM g init (Std.Iter.map f it) ⦃ Q; eQ ⦄
-- Mathlib.Algebra.Group.Action.Hom
MulAction.IsPretransitive.of_compHom : ∀ {M : Type u_4} {N : Type u_5} {α : Type u_6} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : MulAction N α]
  (f : M →* N) [h : MulAction.IsPretransitive M α], MulAction.IsPretransitive N α
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀'_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ),
  AlgebraicTopology.DoldKan.Γ₀'.obj K =
    CategoryTheory.SimplicialObject.Split.mk' (AlgebraicTopology.DoldKan.Γ₀.splitting K)
-- Mathlib.Analysis.Convex.Basic
convex_sInter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {S : Set (Set E)}, (∀ s ∈ S, Convex 𝕜 s) → Convex 𝕜 (⋂₀ S)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.instTransIsBigOTVSIsThetaTVS : {α : Type u_1} →
  {𝕜 : Type u_3} →
    {E : Type u_4} →
      {F : Type u_5} →
        {G : Type u_6} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : AddCommGroup E] →
              [inst_2 : TopologicalSpace E] →
                [inst_3 : Module 𝕜 E] →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : TopologicalSpace F] →
                      [inst_6 : Module 𝕜 F] →
                        [inst_7 : AddCommGroup G] →
                          [inst_8 : TopologicalSpace G] →
                            [inst_9 : Module 𝕜 G] →
                              {l : Filter α} →
                                Trans (Asymptotics.IsBigOTVS 𝕜 l) (Asymptotics.IsThetaTVS 𝕜 l)
                                  (Asymptotics.IsBigOTVS 𝕜 l)
-- Mathlib.Order.Hom.Bounded
TopHom.dual_id : ∀ {α : Type u_2} [inst : LE α] [inst_1 : OrderTop α], TopHom.dual (TopHom.id α) = BotHom.id αᵒᵈ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.leftUnitor_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (𝒯 : CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty C))
  (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) {X₁ X₂ : C} (f : X₁ ⟶ X₂),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ
        (CategoryTheory.CategoryStruct.id 𝒯.cone.pt) f)
      (CategoryTheory.Limits.BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X₂).isLimit).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X₁).isLimit).hom f
-- Mathlib.Algebra.Module.Equiv.Basic
Units.mulLeftLinearEquiv_apply : ∀ (R : Type u_9) {A : Type u_10} [inst : Semiring R] [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] (a : Aˣ) (x : A), ((Units.mulLeftLinearEquiv R A) a) x = ↑a * x
-- Mathlib.Data.Analysis.Topology
Ctop.Realizer.mk.sizeOf_spec : ∀ {α : Type u_6} [T : TopologicalSpace α] [inst : SizeOf α] (σ : Type u_5) (F : Ctop α σ) (eq : F.toTopsp = T),
  sizeOf { σ := σ, F := F, eq := eq } = 1 + sizeOf σ + sizeOf F + sizeOf eq
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun.indepFun_sub_left : ∀ {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {m : MeasurableSpace β} [inst_2 : Sub β]
  [MeasurableSub₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iCondIndepFun m' hm' f μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.CondIndepFun m' hm' (f i - f j) (f k) μ
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- The pregroupoid of all partial maps on a topological space `H`.  -/
continuousPregroupoid : (H : Type u_2) → [inst : TopologicalSpace H] → Pregroupoid H
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.disconnect_normal : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C), S.IsNormal → S.disconnect.IsNormal
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.State.needHeader.sizeOf_spec : ∀ {dir : Std.Http.Protocol.H1.Direction} (a : ℕ), sizeOf (Std.Http.Protocol.H1.Reader.State.needHeader a) = 1 + sizeOf a
-- Mathlib.Topology.Order.ProjIcc
isQuotientMap_projIcc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} {h : a ≤ b} [inst_1 : TopologicalSpace α] [OrderTopology α],
  Topology.IsQuotientMap (Set.projIcc a b h)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.isoMk_hom_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Under X}
  (hr : f.right ≅ g.right)
  (hw : autoParam (CategoryTheory.CategoryStruct.comp f.hom hr.hom = g.hom) CategoryTheory.Under.isoMk._auto_1),
  (CategoryTheory.Under.isoMk hr hw).hom.right = hr.hom
-- Mathlib.Data.Int.Fib.Basic
Int.fib_natCast : ∀ (n : ℕ), Int.fib ↑n = ↑(Nat.fib n)
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddCommSemigroup : {α : Type u_1} → [AddCommSemigroup α] → AddCommSemigroup (Lex α)
-- Mathlib.RingTheory.SimpleModule.Isotypic
IsIsotypicOfType.linearEquiv_fun : ∀ {R : Type u_2} {M : Type u} {S : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup S]
  [inst_3 : Module R M] [inst_4 : Module R S] [IsSemisimpleModule R M] [Module.Finite R M],
  IsIsotypicOfType R M S → ∃ n, Nonempty (M ≃ₗ[R] Fin n → S)
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.sequenceΨ_exact : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k)
  (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (f₂₃ : j ⟶ l)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.sequenceΨ_exact._auto_1),
  (X.sequenceΨ f₁ f₂ f₃ f₁₂ h₁₂ f₂₃ h₂₃ n₀ n₁ hn₁).Exact
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mopMopEquivalence_inverse_obj_unmop_unmop : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C),
  ((CategoryTheory.MonoidalOpposite.mopMopEquivalence C).inverse.obj X).unmop.unmop = X
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformity_eq_comap_nhds_zero' : ∀ (G : Type u_1) [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G],
  uniformity G = Filter.comap (fun p => p.2 + -p.1) (nhds 0)
-- Mathlib.Topology.Algebra.AsymptoticCone
mem_asymptoticCone_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] {v : V} {s : Set P},
  v ∈ asymptoticCone k s ↔ ∃ᶠ (p : P) in AffineSpace.asymptoticNhds k P v, p ∈ s
-- Mathlib.Analysis.Normed.Group.Basic
indiscreteTopology_iff_forall_norm_eq_zero' : ∀ {E : Type u_5} [inst : SeminormedGroup E], IndiscreteTopology E ↔ ∀ (x : E), ‖x‖ = 0
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.deleteEdges_coe_eq : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s : Set (Sym2 ↑G'.verts)),
  G'.coe.deleteEdges s = (G'.deleteEdges (Sym2.map Subtype.val '' s)).coe
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.trans_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8}
  [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁]
  [inst_4 : TopologicalSpace P₁] [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂]
  [inst_8 : TopologicalSpace P₂] [inst_9 : AddCommGroup V₃] [inst_10 : Module k V₃] [inst_11 : AddTorsor V₃ P₃]
  [inst_12 : TopologicalSpace P₃] (e : P₁ ≃ᴬ[k] P₂) (e' : P₂ ≃ᴬ[k] P₃) (p : P₁), (e.trans e') p = e' (e p)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.SignedMeasure.toMeasureOfZeroLE'.eq_1 : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (i : Set α)
  (hi : MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i) (j : Set α)
  (hj : MeasurableSet j), s.toMeasureOfZeroLE' i hi j hj = ↑(NNReal.mk ((MeasureTheory.VectorMeasure.restrict s i) j) ⋯)
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- Given the existence of the appropriate (possibly finite) products and equalizers, we know a limit of
`F` exists.
(This assumes the existence of all equalizers, which is technically stronger than needed.)
 -/
CategoryTheory.Limits.hasLimit_of_equalizer_and_product : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.SmallCategory J]
  (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor F.obj)]
  [CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun f => F.obj f.fst.2)]
  [CategoryTheory.Limits.HasEqualizers C], CategoryTheory.Limits.HasLimit F
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
/-- If `f` is Lipschitz on `uIcc a b`, then `f` is absolutely continuous on `uIcc a b`.  -/
LipschitzOnWith.absolutelyContinuousOnInterval : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {a b : ℝ} {f : ℝ → X} {K : NNReal},
  LipschitzOnWith K f (Set.uIcc a b) → AbsolutelyContinuousOnInterval f a b
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.isBounded_iff_nndist : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α},
  Bornology.IsBounded s ↔ ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → nndist x y ≤ C
-- Mathlib.RingTheory.WittVector.Compare
/-- The unique isomorphism between `ZMod p^n` and `TruncatedWittVector p n (ZMod p)`.

This isomorphism exists, because `TruncatedWittVector p n (ZMod p)` is a finite ring
with characteristic and cardinality `p^n`.
 -/
TruncatedWittVector.zmodEquivTrunc : (p : ℕ) → [hp : Fact (Nat.Prime p)] → (n : ℕ) → ZMod (p ^ n) ≃+* TruncatedWittVector p n (ZMod p)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.nthRootsFinset.congr_simp : ∀ (n n_1 : ℕ),
  n = n_1 →
    ∀ {R : Type u_1} (a a_1 : R),
      a = a_1 →
        ∀ [inst : CommRing R] [inst_1 : IsDomain R], Polynomial.nthRootsFinset n a = Polynomial.nthRootsFinset n_1 a_1
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxRightLinear.δᵣ_unitality_hom : ∀ {D : Type u_1} {D' : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] (F : CategoryTheory.Functor D D') {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D]
  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'] [inst_6 : F.OplaxRightLinear C] (d : D),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso (F.obj d)).hom =
    F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).hom
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.IsRegularEpi.of_epi_of_exists : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X B : C} {f : X ⟶ B}
  [inst_1 : CategoryTheory.Limits.HasPullback f f] [CategoryTheory.Epi f],
  (∀ ⦃Z : C⦄ ⦃g : X ⟶ Z⦄,
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f f) g =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f f) g →
        ∃ u, CategoryTheory.CategoryStruct.comp f u = g) →
    CategoryTheory.IsRegularEpi f