mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashSet.Iterator
/-- Returns a finite iterator over the elements of a hash set.
The iterator yields the elements of the set in order and then terminates.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.HashSet.iter : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Std.HashSet α → Std.Iter α
-- Mathlib.FieldTheory.Galois.Basic
/-- A galois extension with finite galois group is finite dimensional.
The dimension is then equal to the order of the galois group via `IsGalois.card_aut_eq_finrank`.  -/
IsGalois.finiteDimensional_of_finite : ∀ (F : Type u_1) [inst : Field F] (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E] [IsGalois F E]
  [Finite Gal(E/F)], FiniteDimensional F E
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.linear_vaddConst : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (b : P₁), (AffineEquiv.vaddConst k b).linear = LinearEquiv.refl k V₁
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableOn.eventually_differentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s : Set E},
  DifferentiableOn 𝕜 f s → s ∈ nhds x → ∀ᶠ (y : E) in nhds x, DifferentiableAt 𝕜 f y
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.comp.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C}
  (α : X.Hom Y) (β : Y.Hom Z),
  AlgebraicGeometry.PresheafedSpace.comp α β =
    { base := CategoryTheory.CategoryStruct.comp α.base β.base,
      c := CategoryTheory.CategoryStruct.comp β.c ((TopCat.Presheaf.pushforward C β.base).map α.c) }
-- Mathlib.Algebra.Order.Monovary
/-- Two functions antivary iff the rearrangement inequality holds.  -/
antivaryOn_iff_smul_rearrangement : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [IsStrictOrderedModule α β] {f : ι → α} {g : ι → β} {s : Set ι},
  AntivaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g i + f j • g j ≤ f i • g j + f j • g i
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.ext_iff : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOne M] [inst_1 : MulOne N] {f g : M →* N}, f = g ↔ ∀ (x : M), f x = g x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insert k v).contains k = true
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.elabMatchAltViews : Option Bool →
  Array Lean.Elab.Term.Discr →
    Lean.Expr →
      Array Lean.Elab.Term.TermMatchAltView →
        Lean.Elab.TermElabM (Array Lean.Elab.Term.Discr × Lean.Expr × Array (Lean.Meta.Match.AltLHS × Lean.Expr) × Bool)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {a : α}, m.isEmpty = true → m.getKey! a = default
-- Init.Data.Order.FactoriesExtra
Std.compare_eq_lt : ∀ {α : Type u} [inst : Ord α] [inst_1 : LT α] [inst_2 : LE α] [Std.LawfulOrderOrd α] [Std.LawfulOrderLT α] {a b : α},
  compare a b = Ordering.lt ↔ a < b
-- Mathlib.Algebra.Order.Field.Basic
one_div_pow_strictAnti : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α],
  1 < a → StrictAnti fun n => 1 / a ^ n
-- Mathlib.Condensed.TopCatAdjunction
CondensedSet.instUCompactlyGeneratedSpaceCarrierToTopCat : ∀ (X : CondensedSet), UCompactlyGeneratedSpace ↑X.toTopCat
-- Mathlib.Order.RelSeries
RelSeries.toList_cons : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (x : α) (hx : (x, p.head) ∈ r), (p.cons x hx).toList = x :: p.toList
-- Init.Data.SInt.Lemmas
Int16.zero_le_ofNat_of_lt : ∀ {a : ℕ}, a < 2 ^ 15 → 0 ≤ Int16.ofNat a
-- Mathlib.CategoryTheory.Triangulated.Subcategory
/-- The property that `P : ObjectProperty C` is a triangulated subcategory
(of a pretriangulated category `C`).  -/
CategoryTheory.ObjectProperty.IsTriangulated : {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] →
            [CategoryTheory.Pretriangulated C] → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitorCorepresentingIso_hom_app_hom_apply_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (F X : CategoryTheory.Functor C V)
  (a :
    (((CategoryTheory.Functor.whiskeringLeft (C × C) C V).obj (CategoryTheory.MonoidalCategory.tensor C)).comp
          (((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Discrete PUnit.{1} × C) (C × C) V).obj
                ((CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).prod
                  (CategoryTheory.Functor.id C))).comp
            (CategoryTheory.coyoneda.obj
              (Opposite.op
                (CategoryTheory.MonoidalCategory.externalProduct
                  (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)) F))))).obj
      X)
  (X_1 : C),
  ((CategoryTheory.ConcreteCategory.hom
            ((CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitorCorepresentingIso F).hom.app X))
          a).app
      X_1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X_1)).inv
      (((CategoryTheory.CategoryStruct.comp
                (CategoryTheory.prod.leftUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv.toIso.hom
                (TypeCat.ofHom fun g =>
                  CategoryTheory.CategoryStruct.comp g
                    (((CategoryTheory.Functor.whiskeringLeft C C V).map
                          (CategoryTheory.NatIso.ofComponents
                              (fun x => CategoryTheory.MonoidalCategoryStruct.leftUnitor x) ⋯).hom).app
                      X))).hom'
            a).app
        X_1)
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.setOfPred_dual_isBase_eq : ∀ {α : Type u_1} {M : Matroid α}, {B | M✶.IsBase B} = (fun X => M.E \ X) '' {B | M.IsBase B}
-- Mathlib.LinearAlgebra.Complex.Module
Complex.liftAux_apply : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℝ A] (I' : A) (hI' : I' * I' = -1) (z : ℂ),
  (Complex.liftAux I' hI') z = (algebraMap ℝ A) z.re + z.im • I'
-- Init.Data.UInt.Basic
instHModUInt16Nat : HMod UInt16 ℕ UInt16
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.instAlgebraQuotient : (R₁ : Type u_1) →
  [inst : CommSemiring R₁] →
    {A : Type u_5} → [inst_1 : CommRing A] → [Algebra R₁ A] → (I : Ideal A) → Algebra R₁ (A ⧸ I)
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.instUniformContinuousConstSMul : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] (M : Type u_6) [inst_7 : Monoid M] [inst_8 : DistribMulAction M F]
  [inst_9 : SMulCommClass 𝕜₂ M F] [inst_10 : UniformSpace F] [inst_11 : IsUniformAddGroup F]
  [inst_12 : UniformContinuousConstSMul M F] (𝔖 : Set (Set E)),
  UniformContinuousConstSMul M (UniformConvergenceCLM σ F 𝔖)
-- Mathlib.CategoryTheory.GradedObject.Unitor
/-- Given `F : D ⥤ C ⥤ D`, `Y : C`, `e : F.flip.obj Y ≅ 𝟭 D`, `X : GradedObject J D` and
`p : J × I → J` such that `p ⟨j, 0⟩ = j` for all `j`,
this is the (colimit) cofan which shall be used to construct the isomorphism
`mapBifunctorMapObj F p X ((single₀ I).obj Y) ≅ X`, see `mapBifunctorRightUnitor`.  -/
CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan : {C : Type u_1} →
  {D : Type u_2} →
    {I : Type u_3} →
      {J : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
            [inst_2 : Zero I] →
              [inst_3 : DecidableEq I] →
                [inst_4 : CategoryTheory.Limits.HasInitial C] →
                  (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) →
                    (Y : C) →
                      (F.flip.obj Y ≅ CategoryTheory.Functor.id D) →
                        [∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)] →
                          (p : J × I → J) →
                            (∀ (j : J), p (j, 0) = j) →
                              (X : CategoryTheory.GradedObject J D) →
                                (j : J) →
                                  (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj
                                        ((CategoryTheory.GradedObject.single₀ I).obj Y)).CofanMapObjFun
                                    p j
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.le_of_add_le_add_right : ∀ {α : Type u} [inst : Add α] {x y z : WithBot α} [inst_1 : LE α] [AddRightReflectLE α], z ≠ ⊥ → x + z ≤ y + z → x ≤ y
-- Init.Grind.Ring.Basic
Lean.Grind.IsCharP.intCast_eq_zero_iff : ∀ (p : ℕ) {α : Type u} [inst : Lean.Grind.Ring α] [Lean.Grind.IsCharP α p] (x : ℤ), ↑x = 0 ↔ x % ↑p = 0
-- Init.Data.Ord.Basic
List.compare_nil_right_eq_eq : ∀ {α : Type u_1} [inst : Ord α] {xs : List α}, compare xs [] = Ordering.eq ↔ xs = []
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsLinearSet.closure_of_finite : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s : Set M}, s.Finite → IsLinearSet ↑(AddSubmonoid.closure s)
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.lcm_eq_zero_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  {f : β → α} [Nontrivial α], s.lcm f = 0 ↔ ∃ x ∈ s, f x = 0
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.zero : {M : Type u_1} → [inst : Add M] → [Zero M] → (c : AddCon M) → Zero c.Quotient
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- The `L^p` norm of a Schwartz function is controlled by a finite family of Schwartz seminorms.

The maximum index `k` and the constant `C` depend on `p` and `μ`.
 -/
SchwartzMap.eLpNorm_le_seminorm : ∀ (𝕜 : Type u_2) {E : Type u_5} (F : Type u_6) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : MeasurableSpace E] [OpensMeasurableSpace E]
  [inst_6 : NormedField 𝕜] [inst_7 : NormedSpace 𝕜 F] [inst_8 : SMulCommClass ℝ 𝕜 F] (p : ENNReal)
  (μ : autoParam (MeasureTheory.Measure E) SchwartzMap.eLpNorm_le_seminorm._auto_1) [hμ : μ.HasTemperateGrowth],
  ∃ k C,
    ∀ (f : SchwartzMap E F),
      MeasureTheory.eLpNorm (⇑f) p μ ≤ ↑C * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)
-- Std.Data.DHashMap.Lemmas
/-- Simpler variant of `get!_filter` when `LawfulBEq` is available.  -/
Std.DHashMap.Const.get!_filter' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [LawfulBEq α]
  [inst : Inhabited β] {f : α → β → Bool} {k : α},
  Std.DHashMap.Const.get! (Std.DHashMap.filter f m) k = (Option.filter (f k) (Std.DHashMap.Const.get? m k)).get!
-- Mathlib.Data.Nat.Prime.Basic
Nat.Prime.pred_pos : ∀ {p : ℕ}, Nat.Prime p → 0 < p.pred
-- Mathlib.Topology.Compactness.Paracompact
/-- Let `X` be a locally compact sigma compact Hausdorff topological space, let `s` be a closed set
in `X`. Suppose that for each `x ∈ s` the sets `B x : ι x → Set X` with the predicate
`p x : ι x → Prop` form a basis of the filter `𝓝 x`. Then there exists a locally finite covering
`fun i ↦ B (c i) (r i)` of `s` such that all “centers” `c i` belong to `s` and each `r i` satisfies
`p (c i)`.

The notation is inspired by the case `B x r = Metric.ball x r` but the theorem applies to
`nhds_basis_opens` as well. If the covering must be subordinate to some open covering of `s`, then
the user should use a basis obtained by `Filter.HasBasis.restrict_subset` or a similar lemma, see
the proof of `paracompact_of_locallyCompact_sigmaCompact` for an example.

The formalization is based on two [ncatlab](https://ncatlab.org/) proofs:
* [locally compact and sigma compact spaces are paracompact](https://ncatlab.org/nlab/show/locally+compact+and+sigma-compact+spaces+are+paracompact);
* [open cover of smooth manifold admits locally finite refinement by closed balls](https://ncatlab.org/nlab/show/partition+of+unity#ExistenceOnSmoothManifolds).

See also `refinement_of_locallyCompact_sigmaCompact_of_nhds_basis` for a version of this lemma
dealing with a covering of the whole space.

In most cases (namely, if `B c r ∪ B c r'` is again a set of the form `B c r''`) it is possible
to choose `α = X`. This fact is not yet formalized in `mathlib`.  -/
refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set : ∀ {X : Type v} [inst : TopologicalSpace X] [WeaklyLocallyCompactSpace X] [SigmaCompactSpace X] [T2Space X]
  {ι : X → Type u} {p : (x : X) → ι x → Prop} {B : (x : X) → ι x → Set X} {s : Set X},
  IsClosed s →
    (∀ x ∈ s, (nhds x).HasBasis (p x) (B x)) →
      ∃ α c r, (∀ (a : α), c a ∈ s ∧ p (c a) (r a)) ∧ s ⊆ ⋃ a, B (c a) (r a) ∧ LocallyFinite fun a => B (c a) (r a)
-- Init.Data.List.Attach
List.reverse_unattach : ∀ {α : Type u_1} {P : α → Prop} {xs : List (Subtype P)}, xs.unattach.reverse = xs.reverse.unattach
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.instAddActionOfVAddAssocClass.eq_1 : ∀ {M : Type u_3} {X : Type u_4} [inst : AddMonoid M] {S : AddSubmonoid M} [inst_1 : AddOreLocalization.AddOreSet S]
  [inst_2 : AddAction M X] {R : Type u_5} [inst_3 : AddMonoid R] [inst_4 : AddAction R M]
  [inst_5 : VAddAssocClass R M M] [inst_6 : AddAction R X] [inst_7 : VAddAssocClass R M X],
  AddOreLocalization.instAddActionOfVAddAssocClass =
    { toVAdd := AddOreLocalization.instVAddOfVAddAssocClass, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.CategoryTheory.Limits.Creates
/-- Definition 3.3.1 of [Riehl].
We say that `F` creates limits of `K` if, given any limit cone `c` for `K ⋙ F`
(i.e. below) we can lift it to a cone "above", and further that `F` reflects
limits for `K`.

If `F` reflects isomorphisms, it suffices to show only that the lifted cone is
a limit - see `createsLimitOfReflectsIso`.
 -/
CategoryTheory.CreatesLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            CategoryTheory.Functor J C → CategoryTheory.Functor C D → Type (max (max (max (max u₁ u₂) v₁) v₂) w)
-- Mathlib.CategoryTheory.Adjunction.Additive
CategoryTheory.Adjunction.homAddEquiv_apply : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.Additive] (X : C) (Y : D) (f : F.obj X ⟶ Y),
  (adj.homAddEquiv X Y) f = (adj.homEquiv X Y) f
-- Mathlib.FieldTheory.AbelRuffini
IsSolvableByRad.below : {F : Type u_1} →
  {E : Type u_2} →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] → {motive : (a : E) → IsSolvableByRad F a → Prop} → {a : E} → IsSolvableByRad F a → Prop
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.ofList_nil : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v}, Std.DTreeMap.Const.ofList [] cmp = ∅
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs.eq_1 : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] (a : A), CFC.abs a = CFC.sqrt (star a * a)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- `Semiring` instance for `type`  -/
Lean.Meta.Grind.Arith.CommRing.Ring.semiringInst : Lean.Meta.Grind.Arith.CommRing.Ring → Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.boxProdLeft_apply : ∀ {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) (H : SimpleGraph β) (b : β) (a : α), (G.boxProdLeft H b) a = (a, b)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.chromaticNumber_eq_zero_iff : ∀ {V : Type u} {G : SimpleGraph V}, G.chromaticNumber = 0 ↔ IsEmpty V
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- Given `v : HeightOneSpectrum R`, the valuation associated to `v` has the localization of
`R` at `v` as valuation subring.  -/
IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime_eq_valuationSubring : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime K v =
    (IsDedekindDomain.HeightOneSpectrum.valuation K v).valuationSubring
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ResolveSimpIdResult.expr.sizeOf_spec : ∀ (e : Lean.Expr), sizeOf (Lean.Elab.Tactic.ResolveSimpIdResult.expr e) = 1 + sizeOf e
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- Universal property of the intersection of two pre-`0`-hypercovers.  -/
CategoryTheory.PreZeroHypercover.interLift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreZeroHypercover S} →
        {F : CategoryTheory.PreZeroHypercover S} →
          {G : CategoryTheory.PreZeroHypercover S} →
            [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] →
              G.Hom E → G.Hom F → G.Hom (E.inter F)
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
/-- An odd prime `p` is a square in `F` iff the quadratic character of `ZMod p` does not
take the value `-1` on `χ₄#F * #F`.  -/
FiniteField.isSquare_odd_prime_iff : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F],
  ringChar F ≠ 2 →
    ∀ {p : ℕ} [inst_2 : Fact (Nat.Prime p)],
      p ≠ 2 → (IsSquare ↑p ↔ (quadraticChar (ZMod p)) (↑(ZMod.χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F)) ≠ -1)
-- Lean.AuxRecursor
Lean.isAuxRecursorWithSuffix : Lean.Environment → Lean.Name → String → Bool
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- If `c : Cone F` is a limit, then it is a weak limit.
 -/
CategoryTheory.Limits.IsLimit.isWeakLimit : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {C : Type u_3} →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cone F} → CategoryTheory.Limits.IsLimit t → CategoryTheory.Limits.IsWeakLimit t
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.epi_of_cokernel_iso_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X Y : C} {f : X ⟶ Y}
  [inst_3 : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair f 0)]
  (w : CategoryTheory.Limits.cokernel f ≅ 0), CategoryTheory.Epi f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_eq_zero_iff_of_lt_of_lt : ∀ {x : ℝ}, -Real.pi < x → x < Real.pi → (Real.sin x = 0 ↔ x = 0)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- The restriction of scalars by a composition of ring morphisms identifies to the
composition of the restriction of scalars functors.  -/
ModuleCat.restrictScalarsComp : {R₁ : Type u₁} →
  {R₂ : Type u₂} →
    {R₃ : Type u₃} →
      [inst : Ring R₁] →
        [inst_1 : Ring R₂] →
          [inst_2 : Ring R₃] →
            (f : R₁ →+* R₂) →
              (g : R₂ →+* R₃) →
                ModuleCat.restrictScalars (g.comp f) ≅ (ModuleCat.restrictScalars g).comp (ModuleCat.restrictScalars f)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
Differentiable.smul : ∀ {𝕜 : 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}
  {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F] [IsBoundedSMul 𝕜' F]
  [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'}, Differentiable 𝕜 c → Differentiable 𝕜 f → Differentiable 𝕜 (c • f)
-- Mathlib.Algebra.Star.Basic
star_neg : ∀ {R : Type u} [inst : AddGroup R] [inst_1 : StarAddMonoid R] (r : R), star (-r) = -star r
-- Mathlib.FieldTheory.IntermediateField.Basic
toIntermediateField_toSubalgebra : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L),
  S.toIntermediateField ⋯ = S
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k : α},
  (Std.DTreeMap.filter f t).get? k = Option.filter (f k) (t.get? k)
-- Init.Data.List.Count
List.IsSuffix.countP_le : ∀ {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α}, l₁ <:+ l₂ → List.countP p l₁ ≤ List.countP p l₂
-- Mathlib.Order.UpperLower.Closure
IsAntichain.minimal_mem_upperClosure_iff_mem : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Set α} {x : α},
  IsAntichain (fun x1 x2 => x1 ≤ x2) s → (Minimal (fun x => x ∈ upperClosure s) x ↔ x ∈ s)
-- Mathlib.CategoryTheory.Opposites
/-- Given a natural transformation `α : F ⟶ G`, for `F G : C ⥤ Dᵒᵖ`,
taking `unop` of each component gives a natural transformation `G.leftOp ⟶ F.leftOp`.
 -/
CategoryTheory.NatTrans.leftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G : CategoryTheory.Functor C Dᵒᵖ} → (F ⟶ G) → (G.leftOp ⟶ F.leftOp)
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.VersoModuleDocs.DocContext.addPart : Lean.VersoModuleDocs.DocContext✝ →
  ℕ → Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty → Except String Lean.VersoModuleDocs.DocContext✝
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_norm_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
  {g' : α → F'} {l : Filter α}, (f =o[l] fun x => ‖g' x‖) ↔ f =o[l] g'
-- Mathlib.Order.WithBot
WithTop.le_def' : ∀ {α : Type u_1} [inst : LE α] {x y : WithTop α}, x ≤ y ↔ y = ⊤ ∨ ∃ b, ∃ a ≤ b, y = ↑b ∧ x = ↑a
-- Mathlib.FieldTheory.RatFunc.Valuation
RatFunc.inftyValuation.polynomial : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)] {p : Polynomial F},
  p ≠ 0 → RatFunc.inftyValuationDef F ((algebraMap (Polynomial F) (RatFunc F)) p) = WithZero.exp ↑p.natDegree
-- Std.Data.TreeMap.Basic
/-- Given a proof that the tree map is not empty, retrieves the smallest key.
 -/
Std.TreeMap.minKey : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → (t : Std.TreeMap α β cmp) → t.isEmpty = false → α
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Adjunction.coconesIsoComponentHom.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} J] {K : CategoryTheory.Functor J C} (Y : D)
  (t : ((CategoryTheory.cocones J D).obj (Opposite.op (K.comp F))).obj Y),
  adj.coconesIsoComponentHom Y t = { app := fun j => (adj.homEquiv (K.obj j) Y) (t.app j), naturality := ⋯ }