mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.getEntryLT.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} [inst : Ord α] (k : α)
  (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.Ordered → (∃ a ∈ x, compare a k = Ordering.lt) → Sort u_3)
  (size : ℕ) (ky : α) (y : β) (l r : Std.DTreeMap.Internal.Impl α fun x => β)
  (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, compare a k = Ordering.lt)
  (h_1 :
    (x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
      (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, compare a k = Ordering.lt) →
        motive Std.DTreeMap.Internal.Impl.leaf x he)
  (h_2 :
    (size : ℕ) →
      (ky : α) →
        (y : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, compare a k = Ordering.lt) →
                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he),
  (match Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => h_1 x he
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he => h_2 size ky y l r ho he) =
    h_2 size ky y l r ho he
-- Mathlib.Data.Finset.Card
Finset.one_lt_card : ∀ {α : Type u_1} {s : Finset α}, 1 < s.card ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b
-- Mathlib.Probability.Distributions.Gaussian.Fernique
/-- A Gaussian measure with variance zero is a Dirac.  -/
ProbabilityTheory.IsGaussian.eq_dirac_of_variance_eq_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] [CompleteSpace E] [SecondCountableTopology E],
  (∀ (L : StrongDual ℝ E), ProbabilityTheory.variance (⇑L) μ = 0) → μ = MeasureTheory.Measure.dirac (∫ (x : E), x ∂μ)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.find?_toList_eq_none_iff_not_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, List.find? (fun x => cmp x.fst k == Ordering.eq) t.toList = none ↔ k ∉ t
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.WorkGroup.mk.inj : ∀ {fla : Std.Format.FlattenAllowability} {flb : Std.Format.FlattenBehavior} {items : List Std.Format.WorkItem✝}
  {fla_1 : Std.Format.FlattenAllowability} {flb_1 : Std.Format.FlattenBehavior} {items_1 : List Std.Format.WorkItem✝},
  { fla := fla, flb := flb, items := items } = { fla := fla_1, flb := flb_1, items := items_1 } →
    fla = fla_1 ∧ flb = flb_1 ∧ items = items_1
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Given theorem with name `declName` and type of the form `∀ (a_1 ... a_n), lhs = rhs`,
creates an E-matching pattern for it using `addEMatchTheorem n [lhs]`

If `normalizePattern` is true, it applies the `grind` simplification theorems and simprocs to the
pattern.
 -/
Lean.Meta.Grind.mkEMatchEqTheorem : Lean.Name →
  optParam Bool true →
    optParam Bool true → optParam Bool false → optParam Bool false → Lean.MetaM Lean.Meta.Grind.EMatchTheorem
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instDiv : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → [Div M] → Div (l.Germ M)
-- Mathlib.Data.Finset.Sym
Finset.sym_succ : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α] {n : ℕ},
  s.sym (n + 1) = s.sup fun a => Finset.image (Sym.cons a) (s.sym n)
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.monotone'_extensionProductIter : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] {n m : ℕ},
  n ≤ m → P.extensionProductIter n ≤ P.extensionProductIter m
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
SSet.Truncated.Edge.CompStruct.mk.inj : ∀ {X : SSet.Truncated 2}
  {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })}
  {e₀₁ : SSet.Truncated.Edge x₀ x₁} {e₁₂ : SSet.Truncated.Edge x₁ x₂} {e₀₂ : SSet.Truncated.Edge x₀ x₂}
  {simplex : X.obj (Opposite.op { obj := { len := 2 }, property := SSet.Truncated.Edge.CompStruct._proof_1 })}
  {d₂ :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.δ₂ 2 SSet.Truncated.Edge._proof_2 SSet.Truncated.Edge.CompStruct._proof_2).op))
          simplex =
        e₀₁.edge)
      SSet.Truncated.Edge.CompStruct.d₂._autoParam}
  {d₀ :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.δ₂ 0 SSet.Truncated.Edge._proof_2 SSet.Truncated.Edge.CompStruct._proof_2).op))
          simplex =
        e₁₂.edge)
      SSet.Truncated.Edge.CompStruct.d₀._autoParam}
  {d₁ :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.δ₂ 1 SSet.Truncated.Edge._proof_2 SSet.Truncated.Edge.CompStruct._proof_2).op))
          simplex =
        e₀₂.edge)
      SSet.Truncated.Edge.CompStruct.d₁._autoParam}
  {simplex_1 : X.obj (Opposite.op { obj := { len := 2 }, property := SSet.Truncated.Edge.CompStruct._proof_1 })}
  {d₂_1 :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.δ₂ 2 SSet.Truncated.Edge._proof_2 SSet.Truncated.Edge.CompStruct._proof_2).op))
          simplex_1 =
        e₀₁.edge)
      SSet.Truncated.Edge.CompStruct.d₂._autoParam}
  {d₀_1 :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.δ₂ 0 SSet.Truncated.Edge._proof_2 SSet.Truncated.Edge.CompStruct._proof_2).op))
          simplex_1 =
        e₁₂.edge)
      SSet.Truncated.Edge.CompStruct.d₀._autoParam}
  {d₁_1 :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.δ₂ 1 SSet.Truncated.Edge._proof_2 SSet.Truncated.Edge.CompStruct._proof_2).op))
          simplex_1 =
        e₀₂.edge)
      SSet.Truncated.Edge.CompStruct.d₁._autoParam},
  { simplex := simplex, d₂ := d₂, d₀ := d₀, d₁ := d₁ } = { simplex := simplex_1, d₂ := d₂_1, d₀ := d₀_1, d₁ := d₁_1 } →
    simplex = simplex_1
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
intervalIntegral.FTCFilter.pure_le : ∀ {a : outParam ℝ} {outer : Filter ℝ} {inner : outParam (Filter ℝ)} [self : intervalIntegral.FTCFilter a outer inner],
  pure a ≤ outer
-- Mathlib.RingTheory.MvPolynomial.Basic
/-- **Alias** of `MvPolynomial.map_eq_map`. -/
MvPolynomial.mapRange_eq_map : ∀ (σ : Type u) {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (p : MvPolynomial σ R)
  (f : R →+* S), AddMonoidAlgebra.map (↑f) p = (MvPolynomial.map f) p
-- Mathlib.GroupTheory.Finiteness
/-- An additive monoid is finitely generated iff there exists a surjective
homomorphism from a `FreeAddMonoid` on an arbitrary finite type `α` to the monoid.  -/
AddMonoid.fg_iff_exists_freeAddGroup_hom_surjective_finite : ∀ {M : Type u_1} [inst : AddMonoid M], AddMonoid.FG M ↔ ∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- The first projection from the glued scheme into `X`.  -/
AlgebraicGeometry.Scheme.Pullback.p1 : {X Y Z : AlgebraicGeometry.Scheme} →
  (𝒰 : X.OpenCover) →
    (f : X ⟶ Z) →
      (g : Y ⟶ Z) →
        [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] →
          (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).glued ⟶ X
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Set.Finite.map_sInf_of_monotone : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : ConditionallyCompleteLattice β]
  {f : α → β}, Monotone f → ∀ {s : Set α}, s.Nonempty → s.Finite → f (sInf s) = sInf (f '' s)
-- Mathlib.Computability.StateTransition
/-- A "proof" of the fact that `f` eventually reaches `b` when repeatedly evaluated on `a`,
remembering the number of steps it takes.  -/
StateTransition.EvalsTo : {σ : Type u_1} → (σ → Option σ) → σ → Option σ → Type
-- Lean.Elab.InfoTree.Types
Lean.Elab.DocElabKind : Type
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
PresheafOfModules.homEquivOfIsLocallyBijective_symm_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) {N : PresheafOfModules R}
  (hN : CategoryTheory.Presheaf.IsSheaf J N.presheaf) [inst_1 : J.WEqualsLocallyBijective AddCommGrpCat]
  [inst_2 : PresheafOfModules.IsLocallySurjective J f] [inst_3 : PresheafOfModules.IsLocallyInjective J f] (ψ : M₁ ⟶ N),
  (PresheafOfModules.homEquivOfIsLocallyBijective f hN).symm ψ =
    PresheafOfModules.homMk
      ((CategoryTheory.ObjectProperty.isLocal.homEquiv ⋯ N.presheaf hN).symm ((PresheafOfModules.toPresheaf R).map ψ)) ⋯
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃'_obj_obj_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (k j : C)
  {X Y : C} (φ : X ⟶ Y),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃' C).obj k).obj j).map φ =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft j (CategoryTheory.MonoidalCategoryStruct.whiskerLeft k φ)
-- Mathlib.Order.Ideal
Order.sequenceOfCofinals.monotone : ∀ {P : Type u_1} [inst : Preorder P] (p : P) {ι : Type u_2} [inst_1 : Encodable ι] (𝒟 : ι → Order.Cofinal P),
  Monotone (Order.sequenceOfCofinals p 𝒟)
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivial.homeomorphProd.eq_1 : ∀ (B : Type u_1) (F : Type u_2) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F],
  Bundle.Trivial.homeomorphProd B F = (Bundle.TotalSpace.toProd B F).toHomeomorphOfIsInducing ⋯
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurable.measurable_of_complete : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [μ.IsComplete]
  {_m1 : MeasurableSpace β} {f : α → β}, MeasureTheory.NullMeasurable f μ → Measurable f
-- Mathlib.Order.Monotone.Basic
/-- **Alias** of the reverse direction of `antitone_dual_iff`. -/
Antitone.dual : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → Antitone (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.isTorsionFree_of_forall_isRegular : ∀ {R : Type u_1} {M : Type u_2} {A : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : CommRing A] [inst_4 : AddCommMonoid N] [inst_5 : Module A N] [inst_6 : Algebra R A]
  [inst_7 : Module R N] [IsScalarTower R A N] (f : M →ₗ[R] N) (S : Submonoid R),
  (∀ s ∈ S, s ≠ 0 → IsRegular s) →
    ∀ [Module.IsTorsionFree R M] [IsLocalization S A] [IsLocalizedModule S f], Module.IsTorsionFree A N
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_hom_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ C)
  (X_1 : (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ),
  (AugmentedSimplexCategory.equivAugmentedSimplicialObject.unitIso.hom.app X).app X_1 =
    CategoryTheory.CategoryStruct.comp
      (X.map
        (match Opposite.unop X_1 with
          | CategoryTheory.WithInitial.of x => CategoryTheory.Iso.refl (Opposite.op (CategoryTheory.WithInitial.of x))
          | CategoryTheory.WithInitial.star =>
            CategoryTheory.Iso.refl (Opposite.op CategoryTheory.WithInitial.star)).hom)
      (match
          match Opposite.unop X_1 with
          | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x)
          | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star with
        | CategoryTheory.WithTerminal.of x =>
          (CategoryTheory.Iso.refl
                (CategoryTheory.WithTerminal.incl.comp
                  ((CategoryTheory.WithInitial.opEquiv SimplexCategory).inverse.comp X))).app
            x
        | CategoryTheory.WithTerminal.star =>
          CategoryTheory.Iso.refl (X.obj (Opposite.op CategoryTheory.WithInitial.star))).hom
-- Mathlib.CategoryTheory.Grothendieck
/-- Mapping a Grothendieck construction along the whiskering of any natural transformation
`α : F ⟶ G` with the functor `asSmallFunctor : Cat ⥤ Cat` is naturally isomorphic to conjugating
`map α` with the equivalence between `Grothendieck (F ⋙ asSmallFunctor)` and `Grothendieck F`.  -/
CategoryTheory.Grothendieck.mapWhiskerRightAsSmallFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C CategoryTheory.Cat} →
      (α : F ⟶ G) →
        CategoryTheory.Grothendieck.map (CategoryTheory.Functor.whiskerRight α CategoryTheory.Cat.asSmallFunctor) ≅
          (CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence F).functor.comp
            ((CategoryTheory.Grothendieck.map α).comp
              (CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence G).inverse)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The identity determines a cone on the equalizer diagram of `f` and `g` if `f = g`.  -/
CategoryTheory.Limits.idFork : {C : Type u} →
  {X Y : C} → [inst : CategoryTheory.Category.{v, u} C] → {f g : X ⟶ Y} → f = g → CategoryTheory.Limits.Fork f g
-- Mathlib.Topology.UniformSpace.UniformApproximation
/-- A uniform limit on a set of functions which are uniformly continuous on this set is itself
uniformly continuous on this set.  -/
TendstoUniformlyOn.uniformContinuousOn : ∀ {α : Type u_4} {β : Type u_5} {ι : Type u_6} [inst : UniformSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {s : Set α} {p : Filter ι},
  TendstoUniformlyOn F f p s → (∃ᶠ (n : ι) in p, UniformContinuousOn (F n) s) → UniformContinuousOn f s
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.inf_induced : ∀ {α : Type u} {β : Type u_1} [t : TopologicalSpace α] {γ : Type u_2} [s : TopologicalSpace β] {B₁ : Set (Set α)}
  {B₂ : Set (Set β)},
  TopologicalSpace.IsTopologicalBasis B₁ →
    TopologicalSpace.IsTopologicalBasis B₂ →
      ∀ (f₁ : γ → α) (f₂ : γ → β),
        TopologicalSpace.IsTopologicalBasis (Set.image2 (fun x1 x2 => f₁ ⁻¹' x1 ∩ f₂ ⁻¹' x2) B₁ B₂)
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.mapAlgHom_comp : ∀ {R : Type u} {A : Type z} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (C : Type u_3) [inst_5 : Semiring C] [inst_6 : Algebra R C]
  (f : B →ₐ[R] C) (g : A →ₐ[R] B),
  (Polynomial.mapAlgHom f).comp (Polynomial.mapAlgHom g) = Polynomial.mapAlgHom (f.comp g)
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.of_smul_eq_smul : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B}
  (g : G) (w : HNNExtension.NormalWord d), HNNExtension.of g • w = g • w
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.disjoint_left : ∀ {V : Type u} {G H : SimpleGraph V}, Disjoint G H ↔ ∀ (x y : V), G.Adj x y → ¬H.Adj x y
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
DirectedOn.le_csSup_iff : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderSup α] {s : Set α} {a : α},
  DirectedOn (fun x1 x2 => x1 ≤ x2) s → BddAbove s → s.Nonempty → (a ≤ sSup s ↔ ∀ b ∈ upperBounds s, a ≤ b)
-- Mathlib.Algebra.Group.Action.Defs
/-- Note that the `IsScalarTower α β β` typeclass argument is usually satisfied by `Algebra α β`.  -/
smul_mul_assoc : ∀ {α : Type u_5} {β : Type u_6} [inst : Mul β] [inst_1 : SMul α β] [IsScalarTower α β β] (r : α) (x y : β),
  r • x * y = r • (x * y)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.r_mul_max_le : ∀ (z : UpperHalfPlane) {x : Fin 2 → ℤ}, x ≠ 0 → EisensteinSeries.r z * ‖x‖ ≤ ‖↑(x 0) * ↑z + ↑(x 1)‖
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.instEpiCommRingCatResidue : ∀ (X : AlgebraicGeometry.Scheme) (x : ↥X), CategoryTheory.Epi (X.residue x)
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.closure_eq_of_le : ∀ {K : Type u} [inst : DivisionRing K] {s : Set K} {t : Subfield K},
  s ⊆ ↑t → t ≤ Subfield.closure s → Subfield.closure s = t
-- Mathlib.Analysis.Convex.StdSimplex
/-- `stdSimplex ℝ ι` is bounded.  -/
bounded_stdSimplex : ∀ (ι : Type u_1) [inst : Fintype ι], Bornology.IsBounded (stdSimplex ℝ ι)
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.FullSubcategory.category : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (P : CategoryTheory.ObjectProperty C) → CategoryTheory.Category.{v, u} P.FullSubcategory
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.nnnorm_tmul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (x : E) (y : F),
  ‖x ⊗ₜ[𝕜] y‖₊ = ‖x‖₊ * ‖y‖₊
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.Recv.timeout.sizeOf_spec : ∀ {β : Type} [inst : SizeOf β], sizeOf Std.Http.Server.Connection.Recv.timeout✝ = 1
-- Mathlib.Algebra.CubicDiscriminant
Cubic.leadingCoeff_of_c_eq_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a = 0 → P.b = 0 → P.c = 0 → P.toPoly.leadingCoeff = P.d
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_restrict_biUnion_finset_iff : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : ι → Set α) (t : Finset ι)
  (p : α → Prop), (∀ᵐ (x : α) ∂μ.restrict (⋃ i ∈ t, s i), p x) ↔ ∀ i ∈ t, ∀ᵐ (x : α) ∂μ.restrict (s i), p x
-- Init.Data.Nat.Basic
Nat.two_pow_pos : ∀ (w : ℕ), 0 < 2 ^ w
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Revert.and_pure_intro_r : ∀ {σs : List (Type u)} {φ : Prop} {P P' Q : Std.Do.SPred σs}, φ → (P ∧ ⌜φ⌝ ⊣⊢ₛ P') → (P' ⊢ₛ Q) → P ⊢ₛ Q
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.IsAddModHom.vadd_hom_assoc : ∀ {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}
  {M' N' : D} {A : C} {inst_4 : CategoryTheory.AddMonObj A} {inst_5 : CategoryTheory.AddModObj A M'}
  {inst_6 : CategoryTheory.AddModObj A N'} {f : M' ⟶ N'} [self : CategoryTheory.IsAddModHom A f] {Z : D} (h : N' ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd h)
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- **Alias** of the forward direction of `hasDerivAtFilter_iff_hasFDerivAtFilter`. -/
HasDerivAtFilter.hasFDerivAtFilter : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] {f : 𝕜 → F} {f' : F} {L : Filter (𝕜 × 𝕜)} [inst_4 : ContinuousSMul 𝕜 F],
  HasDerivAtFilter f f' L → HasFDerivAtFilter f (ContinuousLinearMap.toSpanSingleton 𝕜 f') L
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.keys_insertIfNew_perm : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β k}, (m.insertIfNew k v).keys.Perm (if k ∈ m then m.keys else k :: m.keys)
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.rightInvSeq_nil : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W), cs.rightInvSeq [] = []
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → Std.DHashMap.Raw.Const.get? (m₁ ∪ m₂) k = Std.DHashMap.Raw.Const.get? m₁ k
-- Lean.Message
Lean.BaseMessage.mk.inj : ∀ {α : Type u} {fileName : String} {pos : Lean.Position} {endPos : Option Lean.Position} {keepFullRange : Bool}
  {severity : Lean.MessageSeverity} {isSilent : Bool} {caption : String} {data : α} {fileName_1 : String}
  {pos_1 : Lean.Position} {endPos_1 : Option Lean.Position} {keepFullRange_1 : Bool} {severity_1 : Lean.MessageSeverity}
  {isSilent_1 : Bool} {caption_1 : String} {data_1 : α},
  { fileName := fileName, pos := pos, endPos := endPos, keepFullRange := keepFullRange, severity := severity,
        isSilent := isSilent, caption := caption, data := data } =
      { fileName := fileName_1, pos := pos_1, endPos := endPos_1, keepFullRange := keepFullRange_1,
        severity := severity_1, isSilent := isSilent_1, caption := caption_1, data := data_1 } →
    fileName = fileName_1 ∧
      pos = pos_1 ∧
        endPos = endPos_1 ∧
          keepFullRange = keepFullRange_1 ∧
            severity = severity_1 ∧ isSilent = isSilent_1 ∧ caption = caption_1 ∧ data = data_1
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- The discriminant of the power basis given by `ζ - 1`. Beware that in the cases `p ^ k = 1` and
`p ^ k = 2` the formula uses `1 / 2 = 0` and `0 - 1 = 0`. It is useful only to have a uniform
result. See also `IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow'`.  -/
IsCyclotomicExtension.Rat.discr_prime_pow' : ∀ {p k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [inst_2 : IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)),
  Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis =
    (-1) ^ ((p ^ k).totient / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
-- Mathlib.Analysis.Calculus.FDeriv.Linear
IsBoundedLinearMap.fderivWithin : ∀ {𝕜 : 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} (h : IsBoundedLinearMap 𝕜 f),
  UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 f s x = IsBoundedLinearMap.toContinuousLinearMap f h
-- Mathlib.Algebra.FiniteSupport.Basic
/-- Eta-expanded form of `Function.HasFiniteSupport.neg` -/
Function.HasFiniteSupport.fun_neg : ∀ {α : Type u_1} {M : Type u_3} [inst : SubtractionMonoid M] {f : α → M},
  Function.HasFiniteSupport f → Function.HasFiniteSupport fun i => -f i
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.eq_zero_iff : ∀ {G : Type u_1} [inst : AddGroup G] {N : AddSubgroup G} [inst_1 : N.Normal] (x : G), ↑x = 0 ↔ x ∈ N
-- Mathlib.Tactic.Translate.Core
/-- The name of the attribute, for example `to_additive` or `to_dual`.  -/
Mathlib.Tactic.Translate.TranslateData.attrName : Mathlib.Tactic.Translate.TranslateData → Lean.Name
-- Mathlib.RingTheory.LinearDisjoint
/-- In a commutative ring, if `A` and `B` are subalgebras which are free modules of finite rank,
such that rank of `A ⊔ B` is equal to the product of the rank of `A` and `B`,
then `A` and `B` are linearly disjoint.  -/
Subalgebra.LinearDisjoint.of_finrank_sup_of_free : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A B : Subalgebra R S}
  [Module.Free R ↥A] [Module.Free R ↥B] [Module.Finite R ↥A] [Module.Finite R ↥B],
  Module.finrank R ↥(A ⊔ B) = Module.finrank R ↥A * Module.finrank R ↥B → A.LinearDisjoint B