mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.FiberBundle.Basic
/-- If an element of `F` is invariant under all coordinate changes, then one can define a
corresponding section of the fiber bundle, which is continuous. This applies in particular to the
zero section of a vector bundle. Another example (not yet defined) would be the identity
section of the endomorphism bundle of a vector bundle.  -/
FiberBundleCore.continuous_const_section : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (v : F),
  (∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v) →
    Continuous
      (have this := fun x => ⟨x, v⟩;
      this)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.concat_nil : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v),
  SimpleGraph.Walk.nil.concat h = SimpleGraph.Walk.cons h SimpleGraph.Walk.nil
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.restrictScalars_eq_bot_iff : ∀ (S : Type u_1) (R : Type u_2) (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M] {p : Submodule R M},
  Submodule.restrictScalars S p = ⊥ ↔ p = ⊥
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_eq_zero_of_dvd_aeval_eq_zero : ∀ {R : Type u} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring B] [inst_2 : Algebra R B] {p q : Polynomial R}
  {x : B}, p ∣ q → (Polynomial.aeval x) p = 0 → (Polynomial.aeval x) q = 0
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_neg_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.Algebra.Order.Monoid.Unbundled.TypeTags
Multiplicative.linearOrder : {α : Type u_1} → [LinearOrder α] → LinearOrder (Multiplicative α)
-- Lean.Elab.DefView
/-- Syntax objects for the binders occurring before `:`, we use them to populate the `InfoTree` when elaborating `valueStx`.  -/
Lean.Elab.DefViewElabHeaderData.binderIds : Lean.Elab.DefViewElabHeaderData → Array Lean.Syntax
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_maxD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → ∀ {fallback : α}, t.get! (t.maxD fallback) = t.maxD fallback
-- Mathlib.CategoryTheory.Functor.FullyFaithful
/-- **Alias** of `CategoryTheory.Functor.Faithful.of_comp_iso`. -/
CategoryTheory.Iso.faithful_of_comp : ∀ {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 : CategoryTheory.Functor D E} {H : CategoryTheory.Functor C E} [H.Faithful] (h : F.comp G ≅ H), F.Faithful
-- Init.System.IO
IO.FS.instLTSystemTime : LT IO.FS.SystemTime
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.lift_unique : ∀ {α : Type u} {β : Type v} [inst : AddGroup β] {f : α → β} (g : FreeAddGroup α →+ β),
  (∀ (x : α), g (FreeAddGroup.of x) = f x) → ∀ {x : FreeAddGroup α}, g x = (FreeAddGroup.lift f) x
-- Mathlib.CategoryTheory.Sites.Descent.IsPrestack
CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} ⦃X₁ X₂ : C⦄
  ⦃M₁ : ↑(F.obj { as := Opposite.op X₁ })⦄ ⦃M₂ : ↑(F.obj { as := Opposite.op X₂ })⦄ ⦃Y : C⦄ ⦃f₁ : Y ⟶ X₁⦄ ⦃f₂ : Y ⟶ X₂⦄
  (φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂),
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom φ (CategoryTheory.CategoryStruct.id Y) f₁ f₂ ⋯ ⋯ = φ
-- Std.Http.Data.Headers.Basic
/-- Serializes a transfer encoding back to a comma-separated header value.
 -/
Std.Http.Header.TransferEncoding.serialize : Std.Http.Header.TransferEncoding → Std.Http.Header.Name × Std.Http.Header.Value
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instAddCommSemigroupOfContinuousAdd.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddCommSemigroup β]
  [inst_3 : ContinuousAdd β],
  ContinuousMap.instAddCommSemigroupOfContinuousAdd =
    { toAddSemigroup := ContinuousMap.instAddSemigroupOfContinuousAdd, add_comm := ⋯ }
-- Mathlib.LinearAlgebra.Dual.Basis
Module.DualBases.eval_of_ne : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {e : ι → M} {ε : ι → Module.Dual R M}, Module.DualBases e ε → Pairwise fun i j => (ε i) (e j) = 0
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.structureMapCLM_top_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {K : TopologicalSpace.Compacts E} {i : ℕ} (f : ContDiffMapSupportedIn E F ⊤ K),
  ⇑((ContDiffMapSupportedIn.structureMapCLM 𝕜 ⊤ i) f) = iteratedFDeriv ℝ i ⇑f
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.Subcomplex.union : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C), D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = ↑E
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.toAddMonoid_inj : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι] {γ : Type u₁}
  [inst_2 : AddCommMonoid γ] {f g : (i : ι) → β i →+ γ}, DirectSum.toAddMonoid f = DirectSum.toAddMonoid g ↔ f = g
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleExpr.node.injEq : ∀ (f : Aesop.Frontend.Feature) (children : Array Aesop.Frontend.RuleExpr) (f_1 : Aesop.Frontend.Feature)
  (children_1 : Array Aesop.Frontend.RuleExpr),
  (Aesop.Frontend.RuleExpr.node f children = Aesop.Frontend.RuleExpr.node f_1 children_1) =
    (f = f_1 ∧ children = children_1)
-- Mathlib.Logic.Function.Basic
cast_bijective : ∀ {α β : Sort u_3} (h : α = β), Function.Bijective (cast h)
-- Mathlib.AlgebraicGeometry.GluingOneHypercover
/-- The 1-hypercover of `D.glued` in the big Zariski site that is given by the
open cover `D.U` from the glue data `D`.
The "covering of the intersection of two such open subsets" is the trivial
covering given by `D.V`.  -/
AlgebraicGeometry.Scheme.GlueData.oneHypercover : (D : AlgebraicGeometry.Scheme.GlueData) → AlgebraicGeometry.Scheme.zariskiTopology.OneHypercover D.glued
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.map_mk : ∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (f : Turing.PointedMap Γ Γ') (l : List Γ),
  Turing.ListBlank.map f (Turing.ListBlank.mk l) = Turing.ListBlank.mk (List.map f.f l)
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- Open subsets of boundaryless manifolds are boundaryless.  -/
ModelWithCorners.BoundarylessManifold.open : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [BoundarylessManifold I M] (u : TopologicalSpace.Opens M),
  BoundarylessManifold I ↥u
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeSet α cmp) (e_t : t = t_1)
  (h : t ≠ ∅), t.min h = t_1.min ⋯
-- Mathlib.Algebra.Ring.Int.Parity
Int.not_odd_zero : ¬Odd 0
-- Mathlib.RepresentationTheory.Intertwining
/-- Equivalence between representations is a bijective intertwining map.  -/
Representation.Equiv : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] → Representation A G V → Representation A G W → Type (max u_3 u_4)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coeMonoidHom.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : MulOneClass α],
  Finset.coeMonoidHom = { toFun := SetLike.coe, map_one' := ⋯, map_mul' := ⋯ }
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.foldM_filterWithPostcondition : ∀ {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [inst_3 : Monad n] [inst_4 : Monad o] [LawfulMonad m] [LawfulMonad n]
  [LawfulMonad o] [inst_8 : Std.IteratorLoop α m n] [inst_9 : Std.IteratorLoop α m o] [Std.LawfulIteratorLoop α m n]
  [Std.LawfulIteratorLoop α m o] [inst_12 : MonadLiftT m n] [inst_13 : MonadLiftT n o] [LawfulMonadLiftT m n]
  [LawfulMonadLiftT n o] {f : β → Std.Iterators.PostconditionT n (ULift.{w, 0} Bool)} {g : δ → β → o δ} {init : δ}
  {it : Std.IterM m β},
  Std.IterM.foldM g init (Std.IterM.filterWithPostcondition f it) =
    Std.IterM.foldM
      (fun d b => do
        let __do_lift ← liftM (f b).run
        if __do_lift.down = true then g d b else pure d)
      init it
-- Mathlib.Order.Monotone.Basic
StrictMono.maximal_of_maximal_image : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
  StrictMono f → ∀ {a : α}, (∀ (p : β), p ≤ f a) → ∀ (x : α), x ≤ a
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher.mk.sizeOf_spec : ∀ {ρ : Type} {pat : ρ} {s : String.Slice} [inst : SizeOf ρ] (currPos : s.Pos),
  sizeOf { currPos := currPos } = 1 + sizeOf currPos
-- Mathlib.RingTheory.FractionalIdeal.Basic
/-- An element of `S` such that `I.den • I = I.num`, see `FractionalIdeal.num` and
`FractionalIdeal.den_mul_self_eq_num`.  -/
FractionalIdeal.den : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} → {P : Type u_2} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → FractionalIdeal S P → ↥S
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.pointwiseAdd : {R : Type u_2} →
  {M : Type u_3} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Add (Submodule R M)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMap_single_apply : ∀ {K : Type u_1} [inst : Field K] (w : NumberField.InfinitePlace K) (x : ℝ),
  ↑(NumberField.mixedEmbedding.fundamentalCone.expMap_single w) x = Real.exp ((↑w.mult)⁻¹ * x)
-- Mathlib.MeasureTheory.Covering.Differentiation
VitaliFamily.ae_tendsto_lintegral_enorm_sub_div_of_integrable : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) {E : Type u_2} [inst_1 : NormedAddCommGroup E] [SecondCountableTopology α] [BorelSpace α]
  [MeasureTheory.IsLocallyFiniteMeasure μ] {f : α → E},
  MeasureTheory.Integrable f μ →
    ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (nhds 0)
-- Mathlib.Geometry.Convex.Hull
Convexity.convexHull_convexHull_union : ∀ (R : Type u_1) {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] (s t : Set X),
  (Convexity.convexHull R) ((Convexity.convexHull R) s ∪ t) = (Convexity.convexHull R) (s ∪ t)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.map_zero : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂), f 0 = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.left_edge : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {x y : CategoryTheory.ComposableArrows C 0}
  (e : SSet.Edge x y), CategoryTheory.ComposableArrows.left e.edge = CategoryTheory.nerveEquiv x
-- Mathlib.Algebra.Order.Positive.Ring
Positive.instMonoidSubtypeLtOfNat : {R : Type u_2} → [inst : Semiring R] → [inst_1 : PartialOrder R] → [IsStrictOrderedRing R] → Monoid { x // 0 < x }
-- Mathlib.Combinatorics.Hindman
Hindman.FP.below : {M : Type u_1} →
  [inst : Semigroup M] →
    {motive : (a : Stream' M) → (a_1 : M) → Hindman.FP a a_1 → Prop} →
      {a : Stream' M} → {a_1 : M} → Hindman.FP a a_1 → Prop
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin_one : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E], F⟮1⟯ = ⊥
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.instIsPreorderIsIndContained : ∀ {α : Type u_4}, IsPreorder (SimpleGraph α) SimpleGraph.IsIndContained
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.RevSplitIterator.toOption.match_1.eq_1 : ∀ {ρ : Type} {ρ_1 : ρ} {σ : String.Slice → Type} [inst : String.Slice.Pattern.ToBackwardSearcher ρ_1 σ]
  {s : String.Slice} (motive : String.Slice.RevSplitIterator ρ_1 s → Sort u_1) (currPos : s.Pos)
  (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s))
  (h_1 :
    (currPos : s.Pos) →
      (s_2 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        motive (String.Slice.RevSplitIterator.operating currPos s_2))
  (h_2 : Unit → motive String.Slice.RevSplitIterator.atEnd),
  (match String.Slice.RevSplitIterator.operating currPos s_1 with
    | String.Slice.RevSplitIterator.operating currPos s => h_1 currPos s
    | String.Slice.RevSplitIterator.atEnd => h_2 ()) =
    h_1 currPos s_1
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetric.id : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  LinearMap.id.IsSymmetric
-- Mathlib.Topology.Inseparable
SeparationQuotient.continuousOn_lift : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
  {hf : ∀ (x y : X), Inseparable x y → f x = f y} {s : Set (SeparationQuotient X)},
  ContinuousOn (SeparationQuotient.lift f hf) s ↔ ContinuousOn f (SeparationQuotient.mk ⁻¹' s)
-- Mathlib.Algebra.Star.Basic
/-- Typeclass for a star operation with is involutive.
 -/
InvolutiveStar : Type u → Type u
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.bound'_sq : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]},
  ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 →
    Filter.Tendsto (fun n => ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen✝ p F a ^ 2 ^ n) Filter.atTop
      (nhds 0)
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.comp_apply : ∀ {M N T : CommMonCat} (f : M ⟶ N) (g : N ⟶ T) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.Topology.UniformSpace.Cauchy
Filter.TotallyBounded.eq_1 : ∀ {α : Type u} [uniformSpace : UniformSpace α] (f : Filter α),
  f.TotallyBounded = ∀ d ∈ uniformity α, ∃ t, t.Finite ∧ d.preimage t ∈ f
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.lt_rpow_inv_iff_of_pos : ∀ {x y z : ℝ}, 0 ≤ x → 0 ≤ y → 0 < z → (x < y ^ z⁻¹ ↔ x ^ z < y)
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
/-- The space of `C^n` functions with values in a space `V` is a module over the space of `C^n`
functions with values in `𝕜`.  -/
ContMDiffMap.module' : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_4} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {N : Type u_6} →
                  [inst_4 : TopologicalSpace N] →
                    [inst_5 : ChartedSpace H N] →
                      {n : WithTop ℕ∞} →
                        {V : Type u_10} →
                          [inst_6 : NormedAddCommGroup V] →
                            [inst_7 : NormedSpace 𝕜 V] →
                              Module (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) N 𝕜 n)
                                (ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V n)
-- Std.Data.HashSet.Basic
Std.HashSet.instForInOfMonad : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → {m : Type v → Type w} → [Monad m] → ForIn m (Std.HashSet α) α
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.AffineCover.mk : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {S : AlgebraicGeometry.Scheme} →
    (I₀ : Type v) →
      (X : I₀ → CommRingCat) →
        (f : (j : I₀) → AlgebraicGeometry.Spec (X j) ⟶ S) →
          (idx : ↥S → I₀) →
            (∀ (x : ↥S), x ∈ Set.range ⇑(f (idx x))) →
              autoParam (∀ (j : I₀), P (f j)) AlgebraicGeometry.Scheme.AffineCover.map_prop._autoParam →
                AlgebraicGeometry.Scheme.AffineCover P S
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.eraseManyEntries.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {ρ : Type w} [inst_1 : ForIn Id ρ ((a : α) × β a)]
  (t : Std.DTreeMap.Internal.Impl α β) (l : ρ) (h : t.Balanced),
  t.eraseManyEntries l h =
    (have r := ⟨t, ⋯⟩;
      do
      let __s ←
        forIn l r fun x __s =>
            let r := __s;
            match x with
            | ⟨a, snd⟩ =>
              have hr := ⋯;
              have r := ⟨(Std.DTreeMap.Internal.Impl.erase a (↑r) hr).impl, ⋯⟩;
              pure (ForInStep.yield r)
      have r : t.IteratedEntryErasureFrom := __s
      pure r).run
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.ringFunc.add : FirstOrder.ringFunc 2
-- Mathlib.FieldTheory.Finite.Polynomial
MvPolynomial.indicator.eq_1 : ∀ {K : Type u_1} {σ : Type u_2} [inst : Fintype K] [inst_1 : Fintype σ] [inst_2 : CommRing K] (a : σ → K),
  MvPolynomial.indicator a = ∏ n, (1 - (MvPolynomial.X n - MvPolynomial.C (a n)) ^ (Fintype.card K - 1))
-- ImportGraph.Imports.RequiredModules
/-- Return the names of the constants used in the specified declarations,
and the constants they use transitively.
 -/
Lean.NameSet.transitivelyUsedConstants : Lean.NameSet → Lean.CoreM Lean.NameSet
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.coconeOfDiagramTerminal_ι_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {X : J} (tX : CategoryTheory.Limits.IsTerminal X) (F : CategoryTheory.Functor J C) (j : J),
  (CategoryTheory.Limits.coconeOfDiagramTerminal tX F).ι.app j = F.map (tX.from j)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
/-- The j-invariant `j` of an elliptic curve, which is invariant under isomorphisms over `R`.
Note that to prove two equal elliptic curves have the same `j`, you need to use `simp_rw`,
as `rw` cannot transfer instance `WeierstrassCurve.IsElliptic` automatically.  -/
WeierstrassCurve.j : {R : Type u} → [inst : CommRing R] → (W : WeierstrassCurve R) → [W.IsElliptic] → R
-- Init.Data.Array.Lemmas
Array.size_filterMap_pos_iff : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Option β},
  0 < (Array.filterMap f xs).size ↔ ∃ x, ∃ (_ : x ∈ xs), ∃ b, f x = some b
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.trans_isBigO : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} {G' : Type u_8} [inst : Norm E] [inst_1 : Norm F]
  [inst_2 : SeminormedAddCommGroup G'] {l : Filter α} {f : α → E} {g : α → F} {k : α → G'},
  f =o[l] g → g =O[l] k → f =o[l] k
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonParameterInformationLabel : Lean.FromJson Lean.Lsp.ParameterInformationLabel
-- Mathlib.Analysis.Analytic.Basic
/-- `p` converges on `ball 0 r`  -/
HasFPowerSeriesWithinOnBall.r_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r → r ≤ p.radius
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingBtwn_mem_set_of_hittingBtwn_lt : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β}
  {n : ι} {ω : Ω} [WellFoundedLT ι] {m : ι},
  MeasureTheory.hittingBtwn u s n m ω < m → u (MeasureTheory.hittingBtwn u s n m ω) ω ∈ s
-- Lean.Declaration
Lean.DefinitionSafety.unsafe.sizeOf_spec : sizeOf Lean.DefinitionSafety.unsafe = 1
-- Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
FirstOrder.Field.ACF_isComplete : ∀ {p : ℕ}, Nat.Prime p ∨ p = 0 → (FirstOrder.Language.Theory.ACF p).IsComplete
-- Mathlib.Computability.DFA
DFA.compl_def : ∀ {α : Type u} {σ : Type v} (M : DFA α σ), Mᶜ = { step := M.step, start := M.start, accept := M.acceptᶜ }
-- Mathlib.Data.Set.NAry
/-- **Alias** of `Set.subset_image2_sdiff_right`. -/
Set.subset_image2_diff_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t t' : Set β},
  Set.image2 f s t \ Set.image2 f s t' ⊆ Set.image2 f s (t \ t')
-- Mathlib.RingTheory.AdicCompletion.Noetherian
instIsHausdorffMaximalIdeal : ∀ {R : Type u_1} [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherianRing R]
  [Module.Finite R M] [inst_5 : IsLocalRing R], IsHausdorff (IsLocalRing.maximalIdeal R) M
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.of_surjective : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsPrecomplete I M], Function.Surjective ⇑(AdicCompletion.of I M)
-- Mathlib.Data.Prod.Lex
Prod.Lex.orderBot : {α : Type u_1} →
  {β : Type u_2} →
    [inst : PartialOrder α] → [inst_1 : Preorder β] → [OrderBot α] → [OrderBot β] → OrderBot (Lex (α × β))
-- Mathlib.Topology.Compactness.Bases
eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open : ∀ {X : Type u_1} {ι : Type u_2} [inst : TopologicalSpace X] (b : ι → Set X),
  TopologicalSpace.IsTopologicalBasis (Set.range b) →
    ∀ (U : Set X), IsCompact U → IsOpen U → ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.instHasAffinePropertyQuasiSeparatedQuasiSeparatedSpaceCarrierCarrierCommRingCat : AlgebraicGeometry.HasAffineProperty @AlgebraicGeometry.QuasiSeparated fun X x x_1 x_2 => QuasiSeparatedSpace ↥X
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.mk.inj : ∀ {toProfinite : Profinite} {group : Group ↑toProfinite.toTop}
  {topologicalGroup : IsTopologicalGroup ↑toProfinite.toTop} {toProfinite_1 : Profinite}
  {group_1 : Group ↑toProfinite_1.toTop} {topologicalGroup_1 : IsTopologicalGroup ↑toProfinite_1.toTop},
  { toProfinite := toProfinite, group := group, topologicalGroup := topologicalGroup } =
      { toProfinite := toProfinite_1, group := group_1, topologicalGroup := topologicalGroup_1 } →
    toProfinite = toProfinite_1 ∧ group ≍ group_1
-- Lean.Meta.Tactic.Cases
/-- Keep applying `cases` on any hypothesis that satisfies `p`.
 -/
Lean.MVarId.casesRec : Lean.MVarId → (Lean.LocalDecl → Lean.MetaM Bool) → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Order.RelIso.Basic
/-- Identity map is a relation isomorphism.  -/
RelIso.refl : {α : Type u_1} → (r : α → α → Prop) → r ≃r r
-- Mathlib.Tactic.SimpIntro
/-- Main loop of the `simp_intro` tactic.
* `g`: the original goal
* `ctx`: the simp context, which is extended with local variables as we enter the binders
* `discharge?`: the discharger
* `more`: if true, we will keep introducing binders as long as we can
* `ids`: the list of binder identifiers
 -/
Mathlib.Tactic.simpIntroCore : Lean.MVarId →
  Lean.Meta.Simp.Context →
    optParam Lean.Meta.Simp.SimprocsArray #[] →
      Option Lean.Meta.Simp.Discharge →
        Bool → List (Lean.TSyntax `Lean.binderIdent) → Lean.Elab.TermElabM (Option Lean.MVarId)