mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.commRingNorm.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr) (e : Lean.Meta.Grind.Arith.CommRing.RingExpr)
  (p : Lean.Grind.CommRing.Poly),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.commRingNorm c e p) = 1 + sizeOf c + sizeOf e + sizeOf p
-- Init.Data.Order.LemmasExtra
/-- This lemma derives a `LawfulOrderLT α` instance from a property involving an `Ord α` instance.
 -/
Std.LawfulOrderLT.of_ord : ∀ (α : Type u) [inst : Ord α] [inst_1 : LT α] [inst_2 : LE α] [Std.LawfulOrderOrd α],
  (∀ (a b : α), a < b ↔ compare a b = Ordering.lt) → Std.LawfulOrderLT α
-- Init.Data.Ord.Array
_private.Init.Data.Ord.Array.0.Array.compareLex.go.eq_1 : ∀ {α : Type u_1} (cmp : α → α → Ordering) (a₁ a₂ : Array α) (i : ℕ),
  Array.compareLex.go✝ cmp a₁ a₂ i =
    if h₁ : a₁.size ≤ i then if a₂.size ≤ i then Ordering.eq else Ordering.lt
    else
      if h₂ : a₂.size ≤ i then Ordering.gt
      else
        match cmp a₁[i] a₂[i] with
        | Ordering.lt => Ordering.lt
        | Ordering.eq => Array.compareLex.go✝ cmp a₁ a₂ (i + 1)
        | Ordering.gt => Ordering.gt
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.fst_apply_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N] (x : N),
  AddMonoid.Coprod.fst (AddMonoid.Coprod.inr x) = 0
-- Mathlib.Order.Hom.Order
OrderHom.orderBot : {α : Type u_1} → {β : Type u_2} → [inst : Preorder α] → [inst_1 : Preorder β] → [OrderBot β] → OrderBot (α →o β)
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.exists_lt_eVariationOn_inter_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {ε : ENNReal}
  {s : Set α}, ε < eVariationOn f s → ∃ a ∈ s, ∃ b ∈ s, a < b ∧ ε < eVariationOn f (s ∩ Set.Icc a b)
-- Mathlib.Algebra.Group.Submonoid.Defs
AddMonoidHom.eqLocusM_same : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N), f.eqLocusM f = ⊤
-- Mathlib.Computability.RegularExpressions
RegularExpression.matchEpsilon.eq_1 : ∀ {α : Type u_1}, RegularExpression.zero.matchEpsilon = false
-- Mathlib.Combinatorics.Enumerative.Catalan.Basic
catalan_succ' : ∀ (n : ℕ), catalan (n + 1) = ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n, catalan ij.1 * catalan ij.2
-- Lean.Meta.ACLt
Lean.Meta.ACLt.ReduceMode.reduce.sizeOf_spec : sizeOf Lean.Meta.ACLt.ReduceMode.reduce = 1
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.isIso_opcyclesMap_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.IsIso φ] [inst_3 : S₁.HasRightHomology]
  [inst_4 : S₂.HasRightHomology], CategoryTheory.IsIso (CategoryTheory.ShortComplex.opcyclesMap φ)
-- Mathlib.CategoryTheory.RepresentedBy
CategoryTheory.Functor.IsRepresentedBy.of_natIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {x : F.obj (Opposite.op X)},
  F.IsRepresentedBy x →
    ∀ {F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (e : F ≅ F'),
      F'.IsRepresentedBy ((CategoryTheory.ConcreteCategory.hom (e.hom.app (Opposite.op X))) x)
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.dual.eq_def : ∀ {α : Type u_1} (x : Ordnode α),
  x.dual =
    match x with
    | Ordnode.nil => Ordnode.nil
    | Ordnode.node s l x r => Ordnode.node s r.dual x l.dual
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  t.WF → ∀ {k : α} (h' : k ∈ t), t.get k h' = k
-- Mathlib.Order.RelIso.Basic
/-- **Alias** of `RelHomClass.irrefl`. -/
RelHomClass.isIrrefl : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_5} [inst : FunLike F α β]
  [RelHomClass F r s] (f : F) [Std.Irrefl s], Std.Irrefl r
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticRelatedInformation.mk.injEq : ∀ (location : Lean.Lsp.Location) (message : String) (location_1 : Lean.Lsp.Location) (message_1 : String),
  ({ location := location, message := message } = { location := location_1, message := message_1 }) =
    (location = location_1 ∧ message = message_1)
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.eq_or_eq_of_isPushout' : ∀ {X₁ X₂ X₃ X₄ : Type u} {t : X₁ ⟶ X₂} {r : X₂ ⟶ X₄} {l : X₁ ⟶ X₃} {b : X₃ ⟶ X₄},
  CategoryTheory.IsPushout t l r b →
    ∀ (x₄ : X₄),
      (∃ x₂, (CategoryTheory.ConcreteCategory.hom r) x₂ = x₄) ∨
        ∃ x₃, (CategoryTheory.ConcreteCategory.hom b) x₃ = x₄ ∧ x₃ ∉ Set.range ⇑(CategoryTheory.ConcreteCategory.hom l)
-- Mathlib.Algebra.Order.Group.Lattice
inv_sup : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulLeftMono α] [MulRightMono α] (a b : α), (a ⊔ b)⁻¹ = a⁻¹ ⊓ b⁻¹
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonLeanFileProgressProcessingInfo.fromJson : Lean.Json → Except String Lean.Lsp.LeanFileProgressProcessingInfo
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
CategoryTheory.PreGaloisCategory.IsFundamentalGroup.transitive_of_isGalois : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} {F : CategoryTheory.Functor C FintypeCat}
  {inst_1 : CategoryTheory.GaloisCategory C} {G : Type u_1} {inst_2 : Group G}
  {inst_3 : (X : C) → MulAction G (F.obj X).obj} {inst_4 : TopologicalSpace G} {inst_5 : IsTopologicalGroup G}
  {inst_6 : CompactSpace G} [self : CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] (X : C)
  [CategoryTheory.PreGaloisCategory.IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The low level tape corresponding to the given tape over alphabet `Γ`.  -/
Turing.TM1to1.trTape' : {Γ : Type u_1} →
  {n : ℕ} →
    {enc : Γ → List.Vector Bool n} →
      [inst : Inhabited Γ] →
        enc default = List.Vector.replicate n false → Turing.ListBlank Γ → Turing.ListBlank Γ → Turing.Tape Bool
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_eq_iff_mk'_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] [inst_5 : Algebra R P]
  [inst_6 : IsLocalization M P] {x₁ x₂ : R} {y₁ y₂ : ↥M},
  IsLocalization.mk' S x₁ y₁ = IsLocalization.mk' S x₂ y₂ ↔ IsLocalization.mk' P x₁ y₁ = IsLocalization.mk' P x₂ y₂
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trNormal.eq_4 : ∀ (x : Turing.PartrecToTM2.Cont') (f fs : Turing.ToPartrec.Code),
  Turing.PartrecToTM2.trNormal (f.cons fs) x =
    Turing.PartrecToTM2.Λ'.push Turing.PartrecToTM2.K'.stack (fun x => some Turing.PartrecToTM2.Γ'.consₗ)
      (Turing.PartrecToTM2.Λ'.move (fun x => false) Turing.PartrecToTM2.K'.main Turing.PartrecToTM2.K'.rev
        (Turing.PartrecToTM2.trNormal f (Turing.PartrecToTM2.Cont'.cons₁ fs x)).copy)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
/-- If the restriction to an `m`-measurable set `s` of a σ-algebra `m` is equal to the restriction
to `s` of another σ-algebra `m₂` (hypothesis `hs`), then `μ[f | m] =ᵐ[μ.restrict s] μ[f | m₂]`.  -/
MeasureTheory.condExp_ae_eq_restrict_of_measurableSpace_eq_on : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : α → E}
  {s : Set α} {m m₂ m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (hm₂ : m₂ ≤ m0)
  [MeasureTheory.SigmaFinite (μ.trim hm)] [MeasureTheory.SigmaFinite (μ.trim hm₂)],
  MeasurableSet s → (∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)) → μ[f | m] =ᵐ[μ.restrict s] μ[f | m₂]
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_rco_eq_none : ∀ {m n i : ℕ}, n ≤ i + m → (m...n).toArray[i]? = none
-- Mathlib.AlgebraicGeometry.Morphisms.LocalIso
AlgebraicGeometry.IsLocalIso.exists_isOpenImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.IsLocalIso f] (x : ↥X),
  ∃ U, x ∈ U ∧ AlgebraicGeometry.IsOpenImmersion (CategoryTheory.CategoryStruct.comp U.ι f)
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- associativity of the tensorator  -/
CategoryTheory.Functor.CoreMonoidal.associativity : ∀ {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 D]
  {F : CategoryTheory.Functor C D} (self : F.CoreMonoidal) (X Y Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (self.μIso X Y).hom (F.obj Z))
      (CategoryTheory.CategoryStruct.comp (self.μIso (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom
        (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (self.μIso Y Z).hom)
        (self.μIso X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom)
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove_castSucc_of_le : ∀ {n : ℕ} (p i : Fin n), p ≤ i → p.castSucc.succAbove i = i.succ
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- The obvious equivalence of categories `(ShortComplex C)ᵒᵖ ≌ ShortComplex Cᵒᵖ`.  -/
CategoryTheory.ShortComplex.opEquiv : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (CategoryTheory.ShortComplex C)ᵒᵖ ≌ CategoryTheory.ShortComplex Cᵒᵖ
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.mateEquiv_symm_apply : ∀ {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} F] {G : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D F}
  {L₁ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} {L₂ : CategoryTheory.Functor E F}
  {R₂ : CategoryTheory.Functor F E} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (β : CategoryTheory.TwoSquare R₁ H G R₂),
  (CategoryTheory.mateEquiv adj₁ adj₂).symm β =
    CategoryTheory.TwoSquare.mk G L₁ L₂ H
      (CategoryTheory.CategoryStruct.comp (G.comp L₂).leftUnitor.inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight adj₁.unit (G.comp L₂))
          (CategoryTheory.CategoryStruct.comp ((L₁.comp R₁).associator G L₂).inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (L₁.associator R₁ G).hom L₂)
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (L₁.whiskerLeft β.natTrans) L₂)
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (L₁.associator H R₂).inv L₂)
                  (CategoryTheory.CategoryStruct.comp ((L₁.comp H).associator R₂ L₂).hom
                    (CategoryTheory.CategoryStruct.comp ((L₁.comp H).whiskerLeft adj₂.counit)
                      (L₁.comp H).rightUnitor.hom))))))))
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstr.sugar : Lean.Meta.Grind.Arith.CommRing.EqCnstr → ℕ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.hasGoodReduction_or_hasMultiplicativeReduction_or_hasAdditiveReduction : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] {W : WeierstrassCurve K}
  [WeierstrassCurve.IsMinimal R W],
  WeierstrassCurve.HasGoodReduction R W ∨
    WeierstrassCurve.HasMultiplicativeReduction R W ∨ WeierstrassCurve.HasAdditiveReduction R W
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.instReprLocalTimeType : Repr Std.Time.TimeZone.LocalTimeType
-- Mathlib.Topology.UniformSpace.Ascoli
/-- Let `X` be a compact topological space, `α` a uniform space, `F : ι → (X → α)` an
equicontinuous family, and `ℱ` a filter on `ι`. Then, `F` tends *uniformly* to `f : X → α` along
`ℱ` iff it tends to `f` *pointwise* along `ℱ`.  -/
Equicontinuous.tendsto_uniformFun_iff_pi : ∀ {ι : Type u_1} {X : Type u_2} {α : Type u_3} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] {F : ι → X → α}
  [CompactSpace X],
  Equicontinuous F →
    ∀ (ℱ : Filter ι) (f : X → α),
      Filter.Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (nhds (UniformFun.ofFun f)) ↔ Filter.Tendsto F ℱ (nhds f)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.pi_rpow_zero : ∀ {α : Type u_1} (f : α → ℝ), f ^ 0 = 1
-- Mathlib.Algebra.QuadraticDiscriminant
/-- A quadratic has no root if its discriminant has no square root.  -/
quadratic_ne_zero_of_discrim_ne_sq : ∀ {R : Type u_1} [inst : CommRing R] {a b c : R},
  (∀ (s : R), discrim a b c ≠ s ^ 2) → ∀ (x : R), a * (x * x) + b * x + c ≠ 0
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_symm_of_eq_add : ∀ {n a b : ℕ}, n = a + b → n.choose a = n.choose b
-- Std.Data.DTreeMap.Basic
/-- Dependent tree maps.

A tree map stores an assignment of keys to values. It depends on a comparator function that
defines an ordering on the keys and provides efficient order-dependent queries, such as retrieval
of the minimum or maximum.

To ensure that the operations behave as expected, the comparator function `cmp` should satisfy
certain laws that ensure a consistent ordering:

* If `a` is less than (or equal) to `b`, then `b` is greater than (or equal) to `a`
and vice versa (see the `OrientedCmp` typeclass).
* If `a` is less than or equal to `b` and `b` is, in turn, less than or equal to `c`, then `a`
is less than or equal to `c` (see the `TransCmp` typeclass).

Keys for which `cmp a b = Ordering.eq` are considered the same, i.e., there can be only one entry
with key either `a` or `b` in a tree map. Looking up either `a` or `b` always yields the same entry,
if any is present. The `get` operations of the _dependent_ tree map additionally require a
`LawfulEqCmp` instance to ensure that `cmp a b = .eq` always implies `a = b`, so that their
respective value types are equal.

To avoid expensive copies, users should make sure that the tree map is used linearly.

Internally, the tree maps are represented as size-bounded trees, a type of self-balancing binary
search tree with efficient order statistic lookups.

For use in proofs, the type `Std.ExtDTreeMap` of extensional dependent tree maps should be
preferred. This type comes with several extensionality lemmas and provides the same functions but
requires a `TransCmp` instance to work with.

These tree maps contain a bundled well-formedness invariant, which means that they cannot
be used in nested inductive types. For these use cases, `Std.DTreeMap.Raw` and
`Std.DTreeMap.Raw.WF` unbundle the invariant from the tree map. When in doubt, prefer
`DTreeMap` over `DTreeMap.Raw`.
 -/
Std.DTreeMap : (α : Type u) → (α → Type v) → autoParam (α → α → Ordering) Std.DTreeMap._auto_1 → Type (max u v)
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)),
  CategoryTheory.CategoryStruct.comp S.moduleCatCyclesIso.inv S.homologyπ =
    CategoryTheory.CategoryStruct.comp S.moduleCatLeftHomologyData.π S.moduleCatHomologyIso.inv
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.le_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [inst_2 : PartialOrder M] {v w : MeasureTheory.VectorMeasure α M}, v ≤ w ↔ ∀ (i : Set α), MeasurableSet i → v i ≤ w i
-- Lean.Elab.Do.Basic
Lean.Elab.Do.ContInfo.returnCont : Lean.Elab.Do.ContInfo → Lean.Elab.Do.ReturnCont
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
/-- Let `S` be a short complex in an abelian category. Let `kf` be a
limit kernel fork of `S.g` and `cc` a limit cokernel cofork of `S.f`.
Let `kf.pt ⟶ H ⟶ cc.pt` be an epi-mono factorization of `kf.ι ≫ cc.π : kf.pt ⟶ cc.pt`.
This is the right homology data expressing `H` as the homology of `S`.  -/
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (S : CategoryTheory.ShortComplex C) →
        {kf : CategoryTheory.Limits.KernelFork S.g} →
          {cc : CategoryTheory.Limits.CokernelCofork S.f} →
            CategoryTheory.Limits.IsLimit kf →
              CategoryTheory.Limits.IsColimit cc →
                {H : C} →
                  {π : kf.pt ⟶ H} →
                    {ι : H ⟶ cc.pt} →
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf)
                            (CategoryTheory.Limits.Cofork.π cc) =
                          CategoryTheory.CategoryStruct.comp π ι →
                        [CategoryTheory.Epi π] → [CategoryTheory.Mono ι] → S.RightHomologyData
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.sup' : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {c c' : ℝ}
  {f : α → E} {g' : α → F'} {l l' : Filter α},
  Asymptotics.IsBigOWith c l f g' → Asymptotics.IsBigOWith c' l' f g' → Asymptotics.IsBigOWith (max c c') (l ⊔ l') f g'
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
/-- Two inertia fields are isomorphic.  -/
IsInertiaField.ringEquiv : (K : Type u_2) →
  (L : Type u_3) →
    {B : Type u_4} →
      [inst : Field K] →
        [inst_1 : Field L] →
          [inst_2 : Algebra K L] →
            [inst_3 : CommRing B] →
              (P : Ideal B) →
                (E : Type u_6) →
                  [inst_4 : Field E] →
                    [inst_5 : Algebra E L] →
                      [inst_6 : MulSemiringAction Gal(L/K) B] →
                        (E' : Type u_9) →
                          [inst_7 : Field E'] →
                            [inst_8 : Algebra E' L] → [IsInertiaField K L P E] → [IsInertiaField K L P E'] → E ≃+* E'
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.instIsIsoH₀Hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S} (e : E ≅ F)
  (i : E.I₀), CategoryTheory.IsIso (e.hom.h₀ i)
-- Mathlib.Probability.CentralLimitTheorem
/-- **Central Limit Theorem:** Given a sequence of random variables `X : ℕ → Ω → ℝ` that are
independent, identically distributed with mean `μ` and variance `v`, and a random variable
`Y : Ω' → ℝ` following `gaussianReal 0 v`, the sequence
`n ↦ (√n)⁻¹ * (∑ k ∈ Finset.range n, X k ω - n * μ)` converges to `Y` in distribution.  -/
ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum_sub : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {P : MeasureTheory.Measure Ω}
  {P' : MeasureTheory.Measure Ω'} {X : ℕ → Ω → ℝ} {Y : Ω' → ℝ} [inst : MeasureTheory.IsProbabilityMeasure P]
  [inst_1 : MeasureTheory.IsProbabilityMeasure P'],
  ProbabilityTheory.HasLaw Y (ProbabilityTheory.gaussianReal 0 (ProbabilityTheory.variance (X 0) P).toNNReal) P' →
    MeasureTheory.MemLp (X 0) 2 P →
      ProbabilityTheory.iIndepFun X P →
        (∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) P P) →
          MeasureTheory.TendstoInDistribution
            (fun n ω => (√↑n)⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * ∫ (x : Ω), X 0 x ∂P)) Filter.atTop Y (fun x => P)
            P'
-- Init.Data.SInt.Basic
instLEInt32 : LE Int32
-- Mathlib.Data.Finsupp.Order
Finsupp.support_sup : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [IsBotZeroClass α]
  [inst_3 : DecidableEq ι] (f g : ι →₀ α), (f ⊔ g).support = f.support ∪ g.support
-- Mathlib.Analysis.InnerProductSpace.OfNorm
Continuous.inner_ : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {f g : ℝ → E}, Continuous f → Continuous g → Continuous fun x => inner_✝ 𝕜 (f x) (g x)
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.prodOpEquiv_unitIso_hom_app : ∀ (C : Type u₃) [inst : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [inst_1 : CategoryTheory.Category.{v₄, u₄} D]
  (X : (C × D)ᵒᵖ), (CategoryTheory.prodOpEquiv C).unitIso.hom.app X = CategoryTheory.CategoryStruct.id X
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdderCarry : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      (aig : Std.Sat.AIG α) → Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig → Std.Sat.AIG.Entrypoint α
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasFDerivWithinAt_fst : ∀ {𝕜 : 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] {p : E × F}
  {s : Set (E × F)}, HasFDerivWithinAt Prod.fst (ContinuousLinearMap.fst 𝕜 E F) s p
-- Mathlib.ModelTheory.Arithmetic.Presburger.Definability
FirstOrder.Language.Formula.iSup.congr_simp : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : Finite α] (f f_1 : α → L.Formula β),
  f = f_1 → FirstOrder.Language.Formula.iSup f = FirstOrder.Language.Formula.iSup f_1
-- Mathlib.Algebra.Module.Congruence.Defs
ModuleCon.instDistribMulActionQuotient : {S : Type u_2} →
  (M : Type u_3) →
    [inst : Monoid S] →
      [inst_1 : AddMonoid M] →
        [inst_2 : DistribMulAction S M] → (c : ModuleCon S M) → DistribMulAction S (ModuleCon.Quotient M c)
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.InvariantForm.apply_root_root_zero_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (B : P.InvariantForm)
  (i j : ι) [IsDomain R] [NeZero 2], (B.form (P.root i)) (P.root j) = 0 ↔ P.pairing i j = 0
-- Mathlib.Data.ZMod.Basic
ZMod.intCast_eq_intCast_iff_dvd_sub : ∀ (a b : ℤ) (c : ℕ), ↑a = ↑b ↔ ↑c ∣ b - a
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.ofMatroid_le_iff : ∀ {α : Type u_1} {M M' : Matroid α}, { toMatroid := M } ≤ { toMatroid := M' } ↔ M.IsRestriction M'
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
dist_triangle4_right : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x₁ y₁ x₂ y₂ : α), dist x₁ y₁ ≤ dist x₁ x₂ + dist y₁ y₂ + dist x₂ y₂
-- Mathlib.Order.CompleteLattice.Basic
iInf_const_mono : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [inst : CompleteLattice α] {a : α} (h : ι → ι'), ⨅ x, a ≤ ⨅ x, a
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.isRegular_iff : ∀ {R : Type u_1} (M : Type u_3) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (rs : List R),
  RingTheory.Sequence.IsRegular M rs ↔ RingTheory.Sequence.IsWeaklyRegular M rs ∧ ⊤ ≠ Ideal.ofList rs • ⊤
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isOpenImmersion : ∀ (D : AlgebraicGeometry.LocallyRingedSpace.GlueData) (i : D.J),
  AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (D.ι i)
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_le_degree : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, q.coeff p.natDegree ≠ 0 → p.degree ≤ q.degree
-- Mathlib.RingTheory.Coalgebra.Basic
Prod.instIsCocomm : ∀ (R : Type u) (A : Type v) (B : Type w) [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : AddCommMonoid B]
  [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : Coalgebra R A] [inst_6 : Coalgebra R B] [Coalgebra.IsCocomm R A]
  [Coalgebra.IsCocomm R B], Coalgebra.IsCocomm R (A × B)
-- Mathlib.Tactic.FunProp.Decl
Mathlib.Meta.FunProp.instInhabitedFunPropDecl.default : Mathlib.Meta.FunProp.FunPropDecl
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.toSimpleFunc_toLp : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α E) (hfi : MeasureTheory.MemLp (⇑f) p μ),
  ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc (f.toLp hfi)) =ᵐ[μ] ⇑f